Semantics and proof-theory of depth bounded Boolean logics. (English) Zbl 1315.03107
Summary: We present a unifying semantical and proof-theoretical framework for investigating depth-bounded approximations to Boolean logic, namely approximations in which the number of nested applications of a single structural rule, representing the classical Principle of Bivalence, is bounded above by a fixed natural number. These approximations provide a hierarchy of tractable logical systems that indefinitely converge to classical propositional logic. The framework we present here brings to light a general approach to logical inference that is quite different from the standard Gentzen-style approaches, while preserving some of their nice proof-theoretical properties, and is common to several proof systems and algorithms, such as KE, KI and Stålmarck’s method.
MSC:
| 03F03 | Proof theory in general (including proof-theoretic semantics) |
| 03B05 | Classical propositional logic |
| 03B35 | Mechanization of proofs and logical operations |
References:
| [1] | Avron, A., Natural 3-valued logics. characterization and proof theory, The Journal of Symbolic Logic, 56, 1, 276-294 (1991) · Zbl 0745.03017 |
| [2] | Avron, A., Non-deterministic matrices and modular semantics of rules, (Beziau, J-Yve, Logica Universalis (2005), Birkäuser), 155-174 |
| [3] | Avron, A., A non-deterministic view of non-classical negation, Studia Logica, 80, 2/3 (2005) · Zbl 1086.03023 |
| [4] | Avron, A.; Lev, I., Canonical propositional Gentzen-type systems, (Gore, R.; Leitsch, A.; Nipkov, T., Automated Reasoning: First Joint International Conference (IJCAR). Automated Reasoning: First Joint International Conference (IJCAR), Lecture Notes in Artificial Intelligence (2001), Springer), 529-544 · Zbl 0988.03011 |
| [5] | Avron, A.; Zamansky, A., Cut elimination and quantification in canonical systems, Studia Logica, 82, 157-176 (2006) · Zbl 1097.03050 |
| [6] | Belnap, N. D., How a computer should think, (Ryle, G., Contemporary Aspects of Philosophy (1976), Oriel Press), 30-55 |
| [7] | Belnap, N. D., A useful four-valued logic, (Dunn, J. M.; Epstein, G., Modern uses of multiple-valued logics (1977), Reidel: Reidel Dordrecht), 8-37 · Zbl 0424.03012 |
| [9] | Björk, M., A first-order extension of Stålmarck’s method, (Sutcliffe, G.; Voronkov, A., LPAR. LPAR, LNAI, vol. 3835 (2005), Springer), 276-291 · Zbl 1143.03333 |
| [10] | Björk, M., First-order Stålmarck. Universal lemmas through branch merges, Journal of Automated Reasoning, 42, 99-122 (2009) · Zbl 1191.68618 |
| [11] | Blamey, S., Partial logic, (Gabbay, D. M.; Guenthner, F., Handbook of Philosophical Logic, vol. 3 (1986), Kluwer), 1-70, Republished in the 2nd edition, volume 5, Kluwer, Dordrecht, 2002 · Zbl 0875.03023 |
| [12] | Cadoli, M.; Schaerf, M., Approximate reasoning and non-omniscient agents, (TARK’92: Proceedings of the 4th Conference on Theoretical Aspects of Reasoning about Knowledge, San Francisco, CA, USA (1992), Morgan Kaufmann Publishers Inc), 169-183 |
| [14] | Cook, S. A., The complexity of theorem-proving procedures, (STOC’71: Proceedings of the Third Annual ACM Symposium on Theory of Computing (1971), ACM Press: ACM Press New York, NY, USA), 151-158 · Zbl 0253.68020 |
| [17] | D’Agostino, M., Are tableaux an improvement on truth tables? Cut-free proofs and bivalence, Journal of Logic, Language and Information, 1, 235-252 (1992) · Zbl 0793.03059 |
| [18] | D’Agostino, M., Tableau methods for classical propositional logic, (D’Agostino, M.; Gabbay, D. M.; Hähnle, R.; Posegga, J., Handbook of Tableaux Methods (1999), Kluwer Academic Publishers), 45-123 · Zbl 0972.03523 |
| [19] | D’Agostino, M., Classical natural deduction, (Artëmov, S. N.; Barringer, H.; d’Avila Garcez, A. S.; Lamb, L. C.; Woods, J., We Will Show Them! (1) (2005), College Publications), 429-468 · Zbl 1279.03077 |
| [20] | D’Agostino, M., Tractable depth-bounded logics and the problem of logical omniscience, (Montagna, F.; Hosni, H., Probability, Uncertainty and Rationality. Probability, Uncertainty and Rationality, CRM series (2010), Springer), 245-275 · Zbl 1206.03018 |
| [22] | D’Agostino, M.; Broda, K.; Mondadori, M., A solution to a problem of Popper, (Alai, M.; Tarozzi, G., Popper Philosopher of Science (2006), Rubbettino), 147-168 |
| [23] | D’Agostino, M.; Floridi, L., The enduring scandal of deduction. Is propositionally logic really uninformative?, Synthese, 167, 271-315 (2009) · Zbl 1172.03003 |
| [24] | D’Agostino, M.; Mondadori, M., The taming of the cut, Journal of Logic and Computation, 4, 285-319 (1994) · Zbl 0806.03037 |
| [26] | Dalal, M., Anytime families of tractable propositional reasoners, Annals of Mathematics and Artificial Intelligence, 22, 297-318 (1998) · Zbl 0905.68115 |
| [27] | Dummett, M., Elements of Intuitionism (1977), Clarendon Press: Clarendon Press Oxford · Zbl 0358.02032 |
| [28] | Epstein, R., Propositional Logics. The semantic Foundations of Logic (2012), Advanced Reasoning Forum |
| [29] | Finger, M., Polynomial approximations of full propositional logic via limited bivalence, (9th European Conference on Logics in Artificial Intelligence, JELIA 2004. 9th European Conference on Logics in Artificial Intelligence, JELIA 2004, Lecture Notes in Artificial Intelligence, vol. 3229 (2004), Springer), 526-538 · Zbl 1111.68675 |
| [30] | Finger, M., Towards polynomial approximations of full proposi- tional logic, (Bazzan, A. L.C.; Labidi, S., XVII Brazilian Symposium on Artificial Intel ligence (SBIA 2004). XVII Brazilian Symposium on Artificial Intel ligence (SBIA 2004), Lecture Notes in Artificial Intel lingence, vol. 3171 (2004), Springer), 11-20 · Zbl 1105.68101 |
| [31] | Finger, M.; Gabbay, D. M., Cut and pay, Journal of Logic, Language and Information, 15, 3, 195-218 (2006) · Zbl 1108.03034 |
| [32] | Finger, M.; Wassermann, R., Approximate and limited reasoning: semantics, proof theory, expressivity and control, Journal of Logic and Computation, 14, 2, 179-204 (2004) · Zbl 1101.68086 |
| [33] | Finger, M.; Wassermann, R., The universe of propositional approximations, Theoretical Computer Science, 355, 2, 153-166 (2006) · Zbl 1088.68162 |
| [34] | Gabbay, D. M.; Woods, J., The new logic, Logic Journal of the IGPL, 9, 2, 141-174 (2001) · Zbl 0984.03032 |
| [35] | Gentzen, G., Unstersuchungen über das logische Schliessen, Mathematische Zeitschrift, 39, 176-210 (1935), English translation in [50] · Zbl 0010.14501 |
| [36] | Gödel, K., Zum intuitionistischen Aussagenkalkül, Anzeiger Akademie der Wissenschaften Wien (Math.-naturwiss. Klasse), 69, 65-66 (1932) · JFM 58.1001.03 |
| [37] | Hähnle, R., Tableaux and related methods, (Robinson, A.; Voronkov, A., Handbook of Automated Reasoning, vol. 1 (2001), North Holland: North Holland Amsterdam), 101-178, (chapter 3) · Zbl 1011.68125 |
| [38] | Hintikka, J., Logic, Language Games and Information. Kantian Themes in the Philosophy of Logic (1973), Clarendon Press: Clarendon Press Oxford · Zbl 0253.02005 |
| [39] | Indrzejczak, A., Natural Deduction, Hybrid Systems and Modal Logics (2010), Springer Verlag · Zbl 1236.03002 |
| [40] | Kleene, S. C., Introduction to Metamatehmatics (1952), North-Holland: North-Holland Amsterdam · Zbl 0047.00703 |
| [43] | Mondadori, M., On the notion of a classical proof, (Temi e prospettive della logica e della filosofia della scienza contemporanee, vol. I (1988), CLUEB: CLUEB Bologna), 211-224 |
| [45] | Mondadori, M., Efficient inverse tableaux, Logic Journal of the IGPL, 3, 6, 939-953 (1995) · Zbl 0838.03040 |
| [46] | Moriconi, E.; Tesconi, L., On inversion principles, History and Philosophy of Logic, 29, 2, 103-113 (2008) · Zbl 1147.03001 |
| [47] | Sequoiah-Grayson, S., The scandal of deduction. Hintikka on the information yield of deductive inferences, The Journal of Philosophical Logic, 37, 1, 67-94 (2008) · Zbl 1149.03009 |
| [48] | Sheeran, M.; Stålmarck, G., A tutorial on Stalmarck’s proof procedure for propositional logic, Formal Methods in System Design, 16, 23-58 (2000) |
| [50] | (Szabo, M., The Collected Papers of Gerhard Gentzen (1969), North-Holland: North-Holland Amsterdam) · Zbl 0209.30001 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
