Skip to main content Skip to main navigation menu Skip to site footer
  • Register
  • Login
  • Language
    • English
    • Język Polski
  • Menu
  • Home
  • Current
  • Archives
  • Online First Articles
  • About
    • About the Journal
    • Submissions
    • Editorial Team
    • Advisory Board
    • Peer Review Process
    • Logic and Logical Philosophy Committee
    • Open Access Policy
    • Privacy Statement
    • Contact
  • Register
  • Login
  • Language:
  • English
  • Język Polski

Logic and Logical Philosophy

Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic
  • Home
  • /
  • Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic
  1. Home /
  2. Archives /
  3. Vol. 25 No. 4 (2016): December /
  4. Articles

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

Authors

  • Alexander Steen Freie Universität Berlin
  • Christoph Benzmüller Stanford University

DOI:

https://doi.org/10.12775/LLP.2016.021

Keywords

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

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.

Author Biographies

Alexander Steen, Freie Universität Berlin

Institute of Computer Science

Christoph Benzmüller, Stanford University

CSLI/Cordula Hall

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

Logic and Logical Philosophy

Downloads

  • PDF

Published

2016-07-26

How to Cite

1.
STEEN, Alexander and BENZMÜLLER, Christoph. Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic. Logic and Logical Philosophy. Online. 26 July 2016. Vol. 25, no. 4, pp. 535-554. [Accessed 2 July 2025]. DOI 10.12775/LLP.2016.021.
  • ISO 690
  • ACM
  • ACS
  • APA
  • ABNT
  • Chicago
  • Harvard
  • IEEE
  • MLA
  • Turabian
  • Vancouver
Download Citation
  • Endnote/Zotero/Mendeley (RIS)
  • BibTeX

Issue

Vol. 25 No. 4 (2016): December

Section

Articles

Stats

Number of views and downloads: 817
Number of citations: 8

Crossref
Scopus
Google Scholar
Europe PMC

Search

Search

Browse

  • Browse Author Index
  • Issue archive

User

User

Current Issue

  • Atom logo
  • RSS2 logo
  • RSS1 logo

Information

  • For Readers
  • For Authors
  • For Librarians

Newsletter

Subscribe Unsubscribe

Language

  • English
  • Język Polski

Tags

Search using one of provided tags:

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

Akademicka Platforma Czasopism

Najlepsze czasopisma naukowe i akademickie w jednym miejscu

apcz.umk.pl

Partners

  • Akademia Ignatianum w Krakowie
  • Akademickie Towarzystwo Andragogiczne
  • Fundacja Copernicus na rzecz Rozwoju Badań Naukowych
  • Instytut Historii im. Tadeusza Manteuffla Polskiej Akademii Nauk
  • Instytut Kultur Śródziemnomorskich i Orientalnych PAN
  • Instytut Tomistyczny
  • Karmelitański Instytut Duchowości w Krakowie
  • Ministerstwo Kultury i Dziedzictwa Narodowego
  • Państwowa Akademia Nauk Stosowanych w Krośnie
  • Państwowa Akademia Nauk Stosowanych we Włocławku
  • Państwowa Wyższa Szkoła Zawodowa im. Stanisława Pigonia w Krośnie
  • Polska Fundacja Przemysłu Kosmicznego
  • Polskie Towarzystwo Ekonomiczne
  • Polskie Towarzystwo Ludoznawcze
  • Towarzystwo Miłośników Torunia
  • Towarzystwo Naukowe w Toruniu
  • Uniwersytet im. Adama Mickiewicza w Poznaniu
  • Uniwersytet Komisji Edukacji Narodowej w Krakowie
  • Uniwersytet Mikołaja Kopernika
  • Uniwersytet w Białymstoku
  • Uniwersytet Warszawski
  • Wojewódzka Biblioteka Publiczna - Książnica Kopernikańska
  • Wyższe Seminarium Duchowne w Pelplinie / Wydawnictwo Diecezjalne „Bernardinum" w Pelplinie

© 2021- Nicolaus Copernicus University Accessibility statement Shop