Abstract
Numerous classical and non-classical logics can be elegantly embedded in Church’s simple type theory, also known as classical higher-order logic. Examples include propositional and quantified multimodal logics, intuitionistic logics, logics for security, and logics for spatial reasoning. Furthermore, simple type theory is sufficiently expressive to model combinations of embedded logics and it has a well understood semantics. Off-the-shelf reasoning systems for simple type theory exist that can be uniformly employed for reasoning within and about embedded logics and logics combinations. In this article we focus on combinations of (quantified) epistemic and doxastic logics and study their application for modeling and automating the reasoning of rational agents. We present illustrating example problems and report on experiments with off-the-shelf higher-order automated theorem provers.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Andrews, P.B.: General models and extensionality. J. Symb. Log. 37, 395–397 (1972)
Andrews, P.B.: General models, descriptions, and choice in type theory. J. Symb. Log. 37, 385–394 (1972)
Andrews, P.B.: Theorem proving via general matings. J. ACM 28(2), 193–214 (1981)
Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd edn. Kluwer Academic Publishers (2002)
Andrews, P.B., Bishop, M., Issar, S., Nesmith, D., Pfenning, F., Xi, H.: TPS: a theorem-proving system for classical type theory. J. Autom. Reason. 16(3), 321–353 (1996)
Andrews, P.B., Brown, C.: TPS: a hybrid automatic-interactive system for developing proofs. J. Appl. Log. 4(4), 367–395 (2006)
Backes, J., Brown, C.E.: Analytic tableaux for higher-order logic with choice. In: Giesl, J., Hähnle, R. (eds.) Proceedings of Automated Reasoning: 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, 16–19 Jul 2010. Lecture Notes in Artificial Intelligence, vol. 6173, pp. 76–90. Springer (2010)
Baldoni, M.: Normal multimodal logics: automatic deduction and logic programming extension. PhD thesis, Universita degli studi di Torino (1998)
Benzmüller, C.: Extensional higher-order paramodulation and RUE-resolution. In: In Proc. of CADE-16. LNAI, number 1632, pp. 399–413. Springer (1999)
Benzmüller, C.: Automating access control logic in simple type theory with LEO-II. In: Gritzalis, D., López, J. (eds.) Emerging Challenges for Security, Privacy and Trust, Proceedings of the 24th IFIP TC 11 International Information Security Conference, SEC 2009, Pafos, Cyprus, 18–20 May 2009. IFIP, vol. 297, pp. 387–398. Springer (2009)
Benzmüller, C.: Combining logics in simple type theory. In: Dix, J., Leite, J., Governatori, G., Jamroga, W. (eds.) Computational Logic in Multi-Agent Systems, Proceedings of the 11th International Workshop, CLIMA XI, Lisbon, Portugal, 16–17 Aug 2010. Lecture Notes in Artificial Intelligence, vol. 6245, pp. 33–48. Springer, Lisbon, Portugal (2010)
Benzmüller, C.: Verifying the modal logic cube is an easy task (for higher-order automated reasoners). In: Siegler, S., Wasser, N. (eds.) Verification, Induction, Termination Analysis—Festschrift for Christoph Walther on the Occasion of His 60th Birthday. LNCS, vol. 6463, pp. 117–128. Springer (2010)
Benzmüller, C., Brown, C.E., Kohlhase, M.: Higher order semantics and extensionality. J. Symb. Log. 69, 1027–1088 (2004)
Benzmüller, C., Kohlhase, M.: LEO—a higher-order theorem prover. In: Kirchner, C., Kirchner, H. (eds.) Automated Deduction—CADE-15, Proceedings of the 15th International Conference on Automated Deduction, Lindau, Germany, 5–10 Jul 1998. Lecture Notes in Artificial Intelligence, number 1421, pp. 139–143. Springer, Lindau, Germany (1998)
Benzmüller, C., Paulson, L.C.: Festschrift in Honor of Peter B. Andrews on His 70th Birthday, chapter Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II. Studies in Logic, Mathematical Logic and Foundations. College Publications (2008)
Benzmüller, C., Paulson, L.C.: Quantified Multimodal Logics in Simple Type Theory. SEKI Report SR–2009–02 (ISSN 1437–4447). SEKI Publications, DFKI Bremen GmbH, Safe and Secure Cognitive Systems, Cartesium, Enrique Schmidt Str. 5, D–28359 Bremen, Germany http://arxiv.org/abs/0905.2435 (2009)
Benzmüller, C., Paulson, L.C.: Multimodal and intuitionistic logics in simple type theory. Log J IGPL 18, 881–892 (2010)
Benzmüller, C., Pease, A.: Progress in automating higher-order ontology reasoning. In: Konev, B., Schmidt, R., Schulz, S. (eds.) Proceedings of the Workshop on Practical Aspects of Automated Reasoning (PAAR-2010), Edinburgh, UK. CEUR Workshop Proceedings (2010)
Benzmüller, C., Pease, A.: Reasoning with embedded formulas and modalities in SUMO. In: Bundy, A., Lehmann, J., Qi, G., Varzinczak, I.J. (eds.) Proceedings of the ECAI-10 Workshop on Automated Reasoning about Context and Ontology Evolution (ARCOE-10), Lisbon, Portugal, 16–17 Aug 2010
Benzmüller, C., Rabe, F., Sutcliffe, G.: THF0—the core TPTP language for classical higher-order logic. In: Baumgartner, P., Armando, A., Gilles, D. (eds.) Proceedings of the 4th International Joint Conference on Automated Reasoning. Lecture Notes in Artificial Intelligence, number 5195, pp. 491–506. Springer (2008)
Benzmüller, C., Theiss, F., Paulson, L., Fietzke, A.: LEO-II—a cooperative automatic theorem prover for higher-order logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.), Automated Reasoning, Proceedings of the 4th International Joint Conference, IJCAR 2008, Sydney, Australia, 12–15 Aug 2008. Lecture Notes in Artificial Intelligence, vol. 5195, pp. 162–170. Springer (2008)
Blackburn, P., van Benthem, J.F.A.K., Wolter, F.: Handbook of Modal Logic, vol. 3 (Studies in Logic and Practical Reasoning). Elsevier Science Inc., New York, NY, USA (2006)
Blackburn, P., de Rijke, M.: Why combine logics? Stud. Log. 59, 5–27 (1995)
Blackburn, P., Marx, M.: Tableaux for quantified hybrid logic. In: Egly, U., Fermüller, C.G. (eds.) Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2002, Copenhagen, Denmark, 30 Jul–1 Aug 2002. Lecture Notes in Computer Science, vol. 2381, pp. 38–52. Springer (2002)
Braüner, T.: Natural deduction for first-order hybrid logic. J. Logic Lang. Inf. 14(2), 173–198, (2005)
Brown, C.: Automated Reasoning in Higher-Order Logic: Set Comprehension and Extensionality in Church’s Type Theory. Studies in Logic: Logic and Cognitive Systems, number 10. College Publications (2007)
Carnielli, W., Coniglio, M.E.: Combining logics. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy, Winter 2008 edition (2008)
Carnielli, W.A., Coniglio, M., Gabbay, D.M., Gouveia, P., Sernadas, C.: Analysis and synthesis of logics: how to cut and paste reasoning systems; electronic version. Applied Logic Series. Springer, Dordrecht (2008)
Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5, 56–68 (1940)
Fitting, M.: Interpolation for first order S5. J. Symb. Log. 67(2), 621–634 (2002)
Gabbay, D.M.: Fibred semantics and the weaving of logics, part 1: Modal and intuitionistic logics. J. Symb. Log. 61(4), 1057–1120 (1996)
Gabbay, D.M., Kurucz, A., Wolter, F., Zakharyaschev, M.: Many-dimensional modal logics: theory and applications. Studies in Logic, vol. 148. Elsevier Science (2003)
Garg, D., Abadi, M.: A modal deconstruction of access control logics. In: Amadio, R. (ed.) Proceedings of the 11th International Conference on the Foundations of Software Science and Computational Structures. Lecture Notes in Computer Science, number 4962, pp. 216–230 (2008)
Garson, J.: Modal logic. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. Winter 2009 edition (2009)
Gödel, K.: Eine interpretation des intuitionistischen aussagenkalküls. Ergebnisse eines Mathematischen Kolloquiums, 8, 39–40 (1933) Also published in Gödel, K.: Collected Works, Volume I, pp. 296–302. Oxford University Press (1986)
Goldblatt, R.: Logics of time and computation. Center for the Study of Language and Information - Lecture Notes, number 7. Leland Stanford Junior University (1992)
Henkin, L.: Completeness in the theory of types. J. Symb. Log. 15, 81–91 (1950)
Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Archer, M., Di Vito, B., Munoz, C. (eds.) Proceedings of the 1st International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics. NASA Technical Reports, number NASA/CP-2003-212448, pp. 56–68 (2003)
Kaminski, M., Smolka, G.: Terminating tableau systems for hybrid logic with difference and converse. J. Logic Lang. Inf. 18(4), 437–464 (2009)
McKinsey, J.C.C., Tarski, A.: Some theorems about the sentential calculi of lewis and heyting. J. Symb. Log. 13, 1–15 (1948)
Miller, D.: A Compact Representation of Proofs. Stud. Log. 46(4), 347–370 (1987)
Nguyen, L.A.: MProlog: an extension of prolog for modal logic programming. In: Demoen, B., Lifschitz, V. (eds.) Logic Programming, Proceedings of the 20th International Conference, ICLP 2004, Saint-Malo, France, 6–10 Sept 2004. Lecture Notes in Computer Science, vol. 3132, pp. 469–470. Springer (2004)
Nguyen, L.A.: Multimodal logic programming. Theor. Comp. Sci. 360, 247–288 (2006)
Nguyen, L.A.: Modal logic programming revisited. J. Appl. Non-Class. Log. 19(2), 167–181 (2009)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, number 2283. Springer (2002)
Prior, A.N.: Past, Present and Future. Clarendon Press, Oxford (1967)
Randell, D.A., Cui, Z., Cohn, A.G.: A spatial logic based on regions and connection. In: Proceedings 3rd International Conference on Knowledge Representation and Reasoning, pp. 165–176 (1992)
Schulz, S.: E—a Brainiac theorem prover. Journal of AI Commun. 15(2/3), 111–126 (2002)
Segerberg, K.: Two-dimensional modal logic. J. Philos. Logic 2(1), 77–96 (1973)
Sutcliffe, G.: TPTP, TSTP, CASC, etc. In: Diekert, V., Volkov, M., Voronkov, A. (eds.) Proceedings of the 2nd International Computer Science Symposium in Russia. Lecture Notes in Computer Science, number 4649, pp. 7–23. Springer (2007)
Sutcliffe, G.: The TPTP World—infrastructure for automated reasoning. In: Clarke, E.M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning—16th International Conference, LPAR-16, Dakar, Senegal, 25 Apr–1 May 2010, Revised Selected Papers. Lecture Notes in Computer Science, vol. 6355, pp. 1–12. Springer (2010)
Sutcliffe, G., Benzmüller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. Journal of Formalized Reasoning 3(1), 1–27 (2010)
Thomason, R.H.: Combinations of tense and modality. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic. Extensions of Classical Logic, vol. 2, pp. 135–165. D. Reidel (1984)
Venema, Y.: In: Goble, L. (ed.) The Blackwell Guide to Philosophical Logic, chapter Venema, Yde, Temporal Logic. Blackwell Publishing http://www.blackwellreference.com/public/book?id=g9780631206934_9780631206934 (2001).
Author information
Authors and Affiliations
Corresponding author
Additional information
This work has been funded by the German Research Foundation (DFG) under grant BE 2501/6-1.
Rights and permissions
About this article
Cite this article
Benzmüller, C. Combining and automating classical and non-classical logics in classical higher-order logics. Ann Math Artif Intell 62, 103–128 (2011). https://doi.org/10.1007/s10472-011-9249-7
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10472-011-9249-7
Keywords
- Classical and non-classical logics
- Quantified multimodal logics
- Logic combinations
- Classical higher-order logic
- Semantic embeddings
- Knowledge representation
- Higher-order automated theorem proving