Automated Proof-searching for Strong Kleene Logic and its Binary Extensions via Correspondence Analysis

Yaroslav Petrukhin, Vasilyi Shangin



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.


proof search; correspondence analysis; three-valued logic; strong Kleene logic; natural deduction; proof theory

Full Text:



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

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.

Popov, V.M., “On a three-valued paracomplete logic” (in Russian), Logical Investigations 9 (2002): 175–178.

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

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

ISSN: 1425-3305 (print version)

ISSN: 2300-9802 (electronic version)

Partnerzy platformy czasopism