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

• Authors: Petrukhin Yaroslav , Shangin Vasilyi
• Languages of publication: EN

Abstracts

EN

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.

Keywords

EN

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

• Publisher: Uniwersytet Mikołaja Kopernika (Nicolaus Copernicus University in Toruń)
• Journal: Logic and Logical Philosophy
• Year: 2019
• Volume: 28
• Issue: 2
• Pages: 223–257

Dates

published

2019-06-15

Contributors

author

Petrukhin Yaroslav

• Department of Logic Lomonosov Moscow State University Moscow, Russia

author

Shangin Vasilyi

• Department of Logic Lomonosov Moscow State University Moscow, Russia

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