Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic

Alexander Steen, Christoph Benzmüller

DOI: http://dx.doi.org/10.12775/LLP.2016.021

Abstract


An embedding of many-valued logics based on SIXTEEN in classical higher-order logic is presented. SIXTEEN generalizes the four-valued set of truth degrees of Dunn/Belnap’s system to a lattice of sixteen truth degrees with multiple distinct ordering relations between them. The theoretical motivation is to demonstrate that many-valued logics, like other non-classical logics, can be elegantly modeled (and even combined) as fragments of classical higher-order logic. Equally relevant are the pragmatic aspects of the presented approach: interactive and automated reasoning in many-valued logics, which have broad applications in computer science, artificial intelligence, linguistics, philosophy and mathematics, become readily enabled with state of the art reasoning tools for classical higher-order logic.

Keywords


many-valued logic; non-classical logic; higher-order logic; automated theorem proving; semantic embedding; automation; meta-logical reasoning

Full Text:

PDF

References


Andrews, P.B., “General models, descriptions, and choice in type theory”, The Journal of Symbolic Logic, 37, 2 (1972): 385–394. DOI: 10.2307/2272981

Andrews, P.B., “General models and extensionality”, The Journal of Symbolic Logic, 37, 2 (1972): 395–397. DOI: 10.2307/2272982

Baaz, M., C. Fermller, and G. Salzer, Handbook of Automated Reasoning, chapter “Automated Deduction in Many-Valued Logics”, Elsevier, 2001.

Barendregt, H.P., W. Dekkers, and R. Statman, Lambda Calculus with Types, Cambridge University Press, 2013. DOI: 10.1017/CBO9781139032636

Belnap, N.D., “A useful four-valued logic”, Chapter 2, pages 5–37, in J.M. Dunn and G. Epstein (eds.), Modern Uses of Multiple-Valued Logic, volume 2 of Episteme, Springer, 1977. DOI: 10.1007/978-94-010-1161-7_2

Belnap, N.D., “How a computer should think”, in A. Anderson, N.D. Belnap, and J.M. Dunn (eds.), Entailment: The Logic of Relevance and Necessity, volume 2, Princeton University Press, 1992.

Benzmüller, C., “Invited talk: On a (quite) universal theorem proving approach and its application in metaphysics”, pages 209–216 in H. De Nivelle (ed.), TABLEAUX 2015, volume 9323 of the series LNAI, Springer, Wrocław, 2015.

Benzmüller, C., D. Gabbay, V. Genovese, and D. Rispoli, “Embedding and automating conditional logics in classical higher-order logic”, Annals of Mathematics and Artificial Intelligence, 66, 1–4 (2012): 257–271. DOI: 10.1007/s10472-012-9320-z

Benzmüller, C., and D. Miller, “Automation of higher-order logic”, pages 215–254 in D.M. Gabbay, J.H. Siekmann, and J. Woods (eds.), Handbook of the History of Logic, Volume 9, “Computational logic”, North Holland, Elsevier, 2014. DOI: 10.1016/B978-0-444-51624-4.50005-8

Benzmüller, C., and L. Paulson, “Quantified multimodal logics in simple type theory”, Logica Universalis, 7, 1 (2013): 7–20. DOI: 10.1007/s11787-012-0052-y

Benzmüller, C., L.C. Paulson, N. Sultana, and F. Theiß, “The higher-order prover LEO-II”, Journal of Automated Reasoning, 55, 4 (2015): 389–404. DOI: 10.1007/s10817-015-9348-y

Benzmüller, C., and D. Scott, “Automating free logic in Isabelle/HOL”, pages 43–50 in G.-M. Greuel, T. Koch, P. Paule, and A. Sommese (eds.), Mathematical Software – ICMS 2016, 5th International Congress, Proceedings, volume 9725 of the series Lecture Notes in Computer Science, Springer, Berlin, 2016. DOI: 10.1007/978-3-319-42432-3_6

Benzmüller, C., L. Weber, and B. Woltzenlogel Paleo, “Computer-assisted analysis of the Anderson-Hájek ontological controversy”, pages 53–54 in R. Souza Silvestre and J.-Y. Béziau (eds.), Handbook of the 1st World Congress on Logic and Religion, Joao Pessoa, Brasil, 2015.

Benzmüller, C., and B. Woltzenlogel Paleo, “Automating Gödel’s ontological proof of God’s existence with higher-order automated theorem provers”, pages 93–98 in T. Schaub, G. Friedrich, and B. O’Sullivan (eds.), ECAI 2014, volume 263 of the series Frontiers in Artificial Intelligence and Applications, IOS Press, 2014.

Benzmüller, C., and B. Woltzenlogel Paleo, “Higher-order modal logics: Automation and applications”, Chapter 2,pages 32–74, in A. Paschke and W. Faber (eds.), Reasoning Web. Web Logic Rules, volume 9203 of the series Lecture Notes in Computer Science, Springer, Berlin, 2015. DOI: 10.1007/978-3-319-21768-0_2

Benzmüller, C., and B. Woltzenlogel Paleo, “Interacting with modal logics in the coq proof assistant”, Chapter 25, pages 398–411, in L.D. Beklemishev and D.V. Musatov (eds.), Computer Science – Theory and Applications, volume 9139 of the series Lecture Notes in Computer Science, Springer, 2015. DOI: 10.1007/978-3-319-20297-6_25

Blanchette, J.C., and T. Nipkow, “Nitpick: A counterexample generator for higher-order logic based on a relational model finder”, Chapter 11, pages 131–146, in Interactive Theorem Proving, volume 6172 of the series Lecture Notes in Computer Science, Springer, Berlin-Heidelberg, 2010. DOI: 10.1007/978-3-642-14052-5_11

Brown, C.E., “Satallax: An automatic higher-order prover”, pages 111–117 in Automated Reasoning, Volume 7364 of the series Lecture Notes in Computer Science, 2012. DOI: 10.1007/978-3-642-31365-3_11

Church, A., “A set of postulates for the foundation of logic”, Annals of Mathematics, 33, 2 (1932): 346–366. DOI: 10.2307/1968337

Church, A., ‘A set of postulates for the foundation of logic. Second paper”, Annals of Mathematics, 34, 4 (1933): 839–864. DOI: 10.2307/1968702

Church, A., “A formulation of the simple theory of types”, The Journal of Symbolic Logic, 5, 2 (1940). DOI: 10.2307/2266170

Dummett, M., “A propositional calculus with denumerable matrix”, The Journal of Symbolic Logic, 24, 2 (1959): 97–106. DOI: 10.2307/2964753

Fitting, M., “Kleene’s logic, generalized”, Journal of Logic and Computation, 1, 6 (1991): 797–810. DOI: 10.1093/logcom/1.6.797

Gödel, K., “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme”, Monatshefte für Mathematik und Physik, 38, 1 (1931): 173–198. DOI: 10.1007/BF01700692

Gödel, K., “Zum intuitionistischen aussagenkalkül”, Ergebnisse eines mathematischen Kolloquiums, 4 (1933): 34–38.

Hähnle, R., Automated Deduction in Multiple-Valued Logics, Clarendon Press, Oxford, 1993.

Hajek, P., Metamathematics of Fuzzy Logic, Kluwer, Dordrecht, 1998. DOI: 10.1007/978-94-011-5300-3

Henkin, L., “Completeness in the theory of types”, The Journal of Symbolic Logic, 15, 2 (1950): 81–91. DOI: 10.2307/2266967

Łukasiewicz, J. “O logice trojwartosciowej”, Ruch Filozoficzny, 5 (1920): 170–171.

Nipkow, T., L.C. Paulson, and M. Wenzel, Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of the series Lecture Notes in Computer Science, Springer, 2002. DOI: 10.1007/3-540-45949-9

Odintsov, S.P., “On axiomatizing Shramko–Wansing’s logic”, Studia Logica, 91, 3 (2009): 407–428. DOI: 10.1007/s11225-009-9181-6

Shramko, Y., and H. Wansing, “Some useful 16-valued logics: How a computer network should think”, Journal of Philosophical Logic, 34, 2 (2005): 121–153. DOI: 10.1007/s10992-005-0556-5

Shramko, Y., and H. Wansing, Truth and Falsehood: An Inquiry into Generalized Logical Values, volume 36 of the series Trends in Logic, Springer, 2012. DOI: 10.1007/978-94-007-0907-2

Shramko, Y., J.M. Dunn, and T. Takenaka, “The trilattice of constructive truth values”, Journal of Logic and Computation, 11, 6 (2001): 761–788. DOI: 10.1093/logcom/11.6.761

Steen, A., and M. Wisniewski, “Embedding of first-order nominal logic into HOL”, pages 337–339 in J.-Y. Beziau, S. Ural, A. Buchsbaum, I. Tasdelen, and V. Kamer (eds.), 5th World Congress and School on Universal Logic (UNILOG’15), Istanbul, 2015.

Steen, A., M. Wisniewski, and C. Benzmüller, “Agent-based HOL reasoning”, Chapter 10, pages 75–81, in G.-M. Greuel, T. Koch, P. Paule, and A. Sommese (eds.), Mathematical Software Û ICMS 2016, volume 9725 of the series Lecture Notes in Computer Science, Springer, 2016. DOI: 10.1007/978-3-319-42432-3_10

Sutcliffe, G., “The TPTP problem library and associated infrastructure: The FOF and CNF Parts, v3.5.0”, Journal of Automated Reasoning, 43, 4 (2009): 337–362. DOI: 10.1007/s10817-009-9143-8

Sutcliffe, G., and C. Benzmüller, “Automated reasoning in higher-order logic using the TPTP THF infrastructure”, Journal of Formalized Reasoning, 3, 1 (2010): 1–27.

Zadeh, L., “Fuzzy sets”, Information and Control, 8, 3 (1965): 338–353. DOI: 10.1016/S0019-9958(65)90241-X




Bookmark and Share




Print ISSN: 1425-3305
Online ISSN: 2300-9802

Partnerzy platformy czasopism