Automated Proof-searching for Strong Kleene Logic and its Binary Extensions via Correspondence Analysis
DOI:
https://doi.org/10.12775/LLP.2018.009Keywords
proof search, correspondence analysis, three-valued logic, strong Kleene logic, natural deduction, proof theoryAbstract
Using the method of correspondence analysis, Tamminga obtains sound and complete natural deduction systems for all the unary and binary truth-functional extensions of Kleene’s strong three-valued logic K3 . In this paper, we extend Tamminga’s result by presenting an original finite, sound and complete proof-searching technique for all the truth-functional binary extensions of K3.References
Andrews, P., “Classical type theory”, pages 967–1007 in Handbook of Automated Reasoning, Elsevier Science Publishers BV, 2001. DOI: 10.1016/B978-044450813-3/50017-5
Asenjo, F.G., “A calculus of antinomies”, Notre Dame Journal of Formal Logic 7 (1966): 103–105. DOI: 10.1305/ndjfl/1093958482
Avron, A., “Natural 3-valued logics — characterization and proof theory”, The Journal of Symbolic Logic 61, 1 (1991): 276–294. DOI: 10.2307/2274919
Baaz, M., C.G. Fermüller, and G. Salzer, “Automated deduction for many-valued logics”, Handbook of Automated Reasoning, Elsevier Science Publishers BV, 2001.
Batens, D., “Paraconsistent extensional propositional logics”, Logique et Analyse 23 (90–91) (1980): 195–234.
Beckert B., Hähnle R., P. Oel, and M. Sulzmann, “The tableau-based theorem prover 3 T A P Version 4.0”, pages 303–307 in M.A. McRobbie, J.K. Slaney (eds.) Automated Deduction — Cade-13, CADE 1996, Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence), 1104, 1996. DOI: 10.1007/3-540-61511-3_95
Bocharov V.A., A.E. Bolotov, A.E. Gorchakov, and V.O. Shangin, “Automated first order natural deduction”, pages 1292–1311 in Proceedings of the 2nd Indian International Conference on Artificial Intelligence (IICAI-05), Puna, India, 2005.
Bochvar, D.A., “Ob odnom trehznachnom ischislenii i ego primenenii k analizu paradoksov klassicheskogo rasshirennogo funkcional’nogo ischislenija” (in Russian), Sbornik: Mathematics 4, 2 (1938): 287–308. English translation: D.A. Bochvar, “On a three-valued logical calculus and its application to the analysis of the paradoxes of the classical extended functional calculus”, History and Philosophy of Logic 2 (1981): 87–112. DOI: 10.1080/01445348108837023
Bolotov, A., A. Basukoski, O. Grigoriev, and V. Shangin, “Natural deduction calculus for linear-time temporal logic”, Lecture Notes in Computer Science 4160 (2006): 56–68. DOI: 10.1007/11853886_7
Bolotov, A., and V. Shangin, “Natural deduction system in paraconsistent setting: Proof search for PCont”, Journal of Intelligent Systems 21 (2012): 1–24. DOI: 10.1515/jisys-2011-0021
Copi, I.M., C. Cohen, and K. McMahon, Introduction to Logic, Fourteenth Edition, Routledge, New York, 2011.
D’Agostino, M., “Are tableaux an improvement on truth-tables? Cut-free proofs and bivalence”, Journal of Logic, Language and Information 1 (1992): 235–252. DOI: 10.1007/BF00156916
Fitting, M. First-Order Logic and Automated Theorem Proving, Springer-Verlag, New York, 1996. DOI: 10.1007/978-1-4684-0357-2
Gabbay, D.M., “What is a logical system?”, pages 179–216 in D.M. Gabbay (ed.), What Is a Logical System?, Clarendon Press, Oxford.
Gödel, K., “Zum intuitionistischen Aussgenkalkül”, Anzeiger der Akademie der Wissenschaften in Wien, 69 (1932): 65–66. English translation: “On the intuitionistic propositional calculus”, pages 300–301 in K. Gödel, Collected Works, Vol. 1., New York, 1986.
Haken, A., “The intractability of resolution”, Theoretical Computer Science 39 (1985): 297–308. DOI: 10.1016/0304-3975(85)90144-6
Hazen, A., and F.J. Pelletier, “Gentzen and Jaśkowski natural deduction: Fundamentally similar but importantly different”, Studia Logica 102 (2014): 1103–1142. DOI: 10.1007/s11225-014-9564-1
Hähnle, R., “Automated theorem proving in multiple-valued logics”, Proc. ISMIS, vol. 93, 1993.
Heyting, A., “Die Formalen Regeln der intuitionistischen Logik. Sitzungsberichte der Preussischen Academie der Wissenschaften zu Berlin”, Berlin, 1930: 42-46. English translation: “The formal rules of intuitionistic logic”, pages 311-328 in P. Mancosu (ed.), From Brouwer to Hilbert. The Debate on the Foundations of Mathematics in the 1920s, Oxford, 1998.
Indrzejczak A., “Introduction”, Studia Logica 102 (2014): 1091–1094. DOI: 10.1007/s11225-014-9560-5
Jaśkowski, S., “Recherches sur le système de la logique intuitioniste”, Actes du Congrès International de Philosophie Scientifique 6 (1936): 58–61. English translation: “Investigations into the system of intuitionistic logic”, Studia Logica 34, 2 (1975): 117–120.
Karpenko, A., and N. Tomova, “Bochvar’s three-valued logic and literal paralogics: Their lattice and functional equivalence”, Logic and Logical Philosophy 26 (2017): 207–235. DOI: 10.12775/LLP.2016.029
Kerber M., and M. Kohlhase, “A mechanization of strong Kleene logic for partial functions”, pages 371–385 in A. Bundy (ed.), Automated Deduction – CADE-12. CADE 1994, Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence), 814, 1994. DOI: 10.1007/3-540-58156-1_26
Kleene, S.C., Introduction to Metamathematics, D. Van Nostrand Company, Inc., New York, Toronto. 1952.
Kleene, S.C., “On a notation for ordinal numbers”, The Journal of Symbolic Logic 3 (1938): 150–155. DOI: 10.2307/2267778
Kooi, B., and A. Tamminga, “Completeness via correspondence for extensions of the logic of paradox”, The Review of Symbolic Logic 5 (2012): 720–730. DOI: 10.1017/S1755020312000196
Li, D., “Unification algorithms for eliminating and introducing quantifiers in natural deduction automated theorem proving”, Journal of Automated Reasoning 18 (1997): 105–134. DOI: 10.1023/A:1005749401809
Łukasiewicz, J., “O logice trójwartościowej”, Ruch Filozoficzny 5 (1920): 170–171. English translation: “On three-valued logic”, pages 87-88 in L. Borkowski (ed.), Jan Łukasiewicz: Selected Works, Amsterdam, North-Holland Publishing Company, 1997.
Marcos, J., “On a problem of da Costa”, pages 53–69 in Essays of the Foundations of Mathematics and Logic, Polimetrica International Scientific Publisher, Monza, Italy, 2005.
McKinsey, J.C.C., “On the generation of the functions C p q and N p of Łukasiewicz and Tarski by means of the single binary operation”, Bulletin of the American Mathematical Society 42 (1936): 849–851. DOI: 10.1090/S0002-9904-1936-06440-2
Monteiro, A. “Construction des algèbres de Łukasiewicz trivalentes dans les algèbres de Boole monadiques. I”, Mathematica Japonica 12 (1967): 1–23.
Pelletier, F.J., “Automated natural deduction in Thinker”, Studia Logica 60 (1998): 3–43. DOI: 10.1023/A:1005035316026
Petrukhin, Y.I., “Correspondence analysis for first degree entailment”, Logical Investigations 22, 1 (2016): 108–124.
Petrukhin, Y.I., “Natural deduction system for three-valued Heyting’s logic”, Moscow University Mathematics Bulletin 72, 3 (2017): 63–66. DOI: 10.3103/S002713221703007X
Pollock, J., “Natural deduction”, an unpublished manuscript is available at http://johnpollock.us/ftp/OSCAR-web-page/PAPERS/Natural-Deduction.pdf
Petrukhin, Y., and V. Shangin, “Automated correspondence analysis for the binary extensions of the logic of paradox”, The Review of Symbolic Logic 10, 4 (2017): 756–781. DOI: 10.1017/S1755020317000156
Petrukhin, Y., and V. Shangin, “Natural three-valued logics characterized by natural deduction”, Logique et Analyse, accepted.
Popov, V.M., “Between the logic Par and the set of all formulae” (in Russian), pages 93–95 in The Proceeding of the 6 th Smirnov Readings in logic, Contemporary notebooks, Moscow, 2009. http://smirnovreadings.ru/en/archive/7/
Popov, V.M., “On a three-valued paracomplete logic” (in Russian), Logical Investigations 9 (2002): 175–178. https://iphras.ru/uplfile/logic/log09/LI9_Popov.pdf
Portoraro, F. “Symlog automated advice in Fitch-style proof construction”, pages 802–806 in A. Bundy (ed.) Automated Deduction — CADE-12. CADE 1994, Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence), 814, 1994. DOI: 10.1007/3-540-58156-1_64
Priest, G., “Paraconsistent logic”, in M. Gabbay and F. Guenthner (eds.), Handbook of Philosophical Logic, vol. 6, Second Edition, Dordrecht, Kluwer, 2002. DOI: 10.1007/978-94-017-0460-1_4
Priest, G., “The logic of paradox”, Journal of Philosophical Logic 8 (1979): 219–241. DOI: 10.1007/BF00258428
Rescher, N., Many-Valued Logic, New York, McGraw Hill, 1969.
Sahlqvist, H., “Completeness and correspondence in the first and second order semantics for modal logic”, pages 110–143 in S. Kanger (ed.), Proceeding of the Third Scandinavian Logic Symposium, Amsterdam, North-Holland Publishing Company, 1975.
Sette, A.M., “On propositional calculus P 1 ”, Mathematica Japonica 18 (1973): 173–180.
Sette, A.M., and W.A. Carnielli, “Maximal weakly-intuitionistic logics”, Studia Logica 55 (1995): 181–203. DOI: 10.1007/BF01053037
Sieg, W. and J. Byrnes, “Normal natural deduction proofs (in classical logic)”, Studia Logica 60 (1998): 67–106. DOI: 10.1023/A:1005091418752
Shangin, V.O., “A precise definition of an inference (by the example of natural deduction systems for logics I hα,βi )”, Logical Investigations 23, 1 (2017): 83–104. DOI: 10.21146/2074-1472-2017-23-1-83-104
Shestakov, V.I., “Modelling operations of propositional calculus through the relay contact circuit” (in Russian), in E.Y. Kolman, G.N. Povarov, P.V. Tavanets, and S.A. Yanovskaya (eds.), Logical investigations, 1959.
Shestakov, V.I., “On the relationship between certain three-valued logical calculi” (in Russian), Uspekhi Mat. Nauk 19, 2, 116 (1964): 177–181 (available at http://www.mathnet.ru/links/573d2c9a26538eb817452537a0e26733/rm6197.pdf).
Shestakov, V. I., “On one fragment of D.A. Bochvar’s calculus” (in Russian), Information Issues of Semiotics, Linguistics and Automatic Translation VINITI, 1 (1971): 102–115.
Sieg, W., and F. Pfenning, “Note by the guest editors”, Studia Logica 60 (1998): 1. DOI: 10.1023/A:1005065031956
Słupecki J., G. Bryll, and T. Prucnal, “Some remarks on the three-valued logic of J. Łukasiewicz”, Studia Logica 21 (1967): 45–70. DOI: 10.1007/BF02123418
Steen, A., and C. Benzmüller., “Sweet SIXTEEN: Automation via embedding into classical higher-order logic”, Logic and Logical Philosophy 25, 4 (2016): 535–554. DOI: 10.12775/LLP.2016.021
Tamminga, A., “Correspondence analysis for strong three-valued logic”, Logical Investigations 20 (2014): 255–268.
Tomova, N.E., “A lattice of implicative extensions of regular Kleene’s logics”, Report on Mathematical Logic 47 (2012): 173–182. DOI: 10.4467/20842589RM.12.008.0689
Tomova, N.E., “Erratum to: Natural implication and modus ponens principle”, Logical Investigations 21, 2 (2015): 186–187.
Tomova, N.E., “Natural implication and modus ponens principle”, Logical Investigations 21, 1 (2015): 138–143.
van Benthem, J., “Modal correspondence theory”, PhD Thesis, Universiteit van Amsterdam, Amsterdam, 1976.
van Benthem, J., “Correspondence theory”, pages 325–408 in D.M. Gabbay and F. Guenthner (eds), Handbook of Philosophical Logic, vol. 3, second edition, Dordrecht, Kluwer Academic Publishers, 2001. DOI: 10.1007/978-94-017-0454-0
Downloads
Published
How to Cite
Issue
Section
Stats
Number of views and downloads: 704
Number of citations: 6
