## Quantified multimodal logics in simple type theory.(English)Zbl 1334.03014

Summary: We present an embedding of quantified multimodal logics into simple type theory and prove its soundness and completeness. A correspondence between $$QK\pi$$ models for quantified multimodal logics and Henkin models is established and exploited. Our embedding supports the application of off-the-shelf higher-order theorem provers for reasoning within and about quantified multimodal logics. Moreover, it provides a starting point for further logic embeddings and their combinations in simple type theory.

### MSC:

 03B45 Modal logic (including the logic of norms) 03B15 Higher-order logic; type theory (MSC2010)

### Software:

Isabelle/HOL; Nitpick; HOL; LEO-II; TPS; ETPS
Full Text:

### References:

 [1] Andrews P.B.: General models and extensionality. J. Symb. Logic 37, 395–397 (1972) · Zbl 0264.02050 [2] Andrews P.B.: General models, descriptions, and choice in type theory. J. Symb. Logic 37, 385–394 (1972) · Zbl 0264.02049 [3] Andrews P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd edn. Kluwer, Dordrecht (2002) · Zbl 1002.03002 [4] Andrews, P.B.: Church’s type theory. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. Center for the Study of Language and Information, Stanford University (2009). http://plato.stanford.edu/archives/spr2009/entries/type-theory-church/ [5] Andrews P.B., Brown C.E.: TPS: a hybrid automatic-interactive system for developing proofs. J. Appl. Logic 4(4), 367–395 (2006) · Zbl 1107.68091 [6] Armando, A., Baumgartner, P., Dowek, G. (eds.): Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12–15. Proceedings, LNCS, vol. 5195. Springer, Berlin (2008) · Zbl 1149.68003 [7] 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, 24th IFIP TC 11 International Information Security Conference, SEC 2009, Pafos, Cyprus, May 18–20. Proceedings, IFIP, vol. 297, pp. 387–398. Springer, Berlin (2009) [8] Benzmüller, C.: Simple type theory as framework for combining logics. Contest paper presented at the World Congress and School on Universal Logic III (UNILOG’2010), Lisbon, Portugal (2010). http://arxiv.org/abs/1004.5500 [9] Benzmüller C., Brown C.E., Kohlhase M.: Higher order semantics and extensionality. J. Symb. Logic 69, 1027–1088 (2004) · Zbl 1071.03024 [10] Benzmüller C., Paulson L.C.: Exploring properties of normal multimodal logics in simple type theory with LEO-II. In: Benzmüller, C., Brown, C.E., Siekmann, J., Statman, R. (eds) Festschrift in Honor of Peter B Andrews on His 70th Birthday, Studies in Logic, Mathematical Logic and Foundations., College Publications, London (2008) · Zbl 1227.03017 [11] Benzmüller C., Paulson L.C.: Multimodal and intuitionistic logics in simple type theory. Logic J. IGPL 18(6), 881–892 (2010) · Zbl 1222.03023 [12] Benzmüller, C., Theiss, F., Paulson, L.C., Fietzke, A.: LEO-II–a cooperative automatic theorem prover for higher-order logic. In: Armondo, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12–15. Proceedings, LNCS, vol. 5195. Springer, Berlin, pp 162–170 (2008) · Zbl 1165.68446 [13] Blanchette J.C., Nipkow T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds) First International Conference on Interactive Theorem Proving (ITP 2010), LNCS, vol. 6172., pp. 131–146. Springer, Berlin (2010) · Zbl 1291.68326 [14] Bull R.A.: On modal logic with propositional quantifiers. J. Symb. Logic 34(2), 257–263 (1969) · Zbl 0184.28101 [15] Church A.: A formulation of the simple theory of types. J. Symb. Logic 5, 56–68 (1940) · Zbl 0023.28901 [16] Fine K.: Propositional quantifiers in modal logic. Theoria 36, 336–346 (1970) · Zbl 0302.02005 [17] Fine K.: Failures of the interpolation lemma in quantified modal logic. J. Symb. Logic 44(2), 201–206 (1979) · Zbl 0415.03015 [18] Fitting M.: Interpolation for first order S5. J. Symb. Logic 67(2), 621–634 (2002) · Zbl 1009.03013 [19] Fitting M.: Types, Tableaus, and Gödel’s God. Kluwer, Dordrecht (2002) · Zbl 1038.03001 [20] Fitting M., Mendelsohn R.L.: First-order modal logic. Kluwer, Dordrecht (1998) · Zbl 1025.03001 [21] Henkin L.: Completeness in the theory of types. J. Symb. Logic 15, 81–91 (1950) · Zbl 0039.00801 [22] Hughes G., Cresswell M.: A New Introduction to Modal Logic. Routledge, London (1996) · Zbl 0855.03002 [23] Kaminski M., Smolka G.: Terminating tableau systems for hybrid logic with difference and converse. J. Log. Lang. Inf. 18(4), 437–464 (2009) · Zbl 1188.03013 [24] Kaplan D.: S5 with quantifiable propositional variables. J. Symb. Logic 35, 355 (1970) [25] Kremer P.: On the complexity of propositional quantification in intuitionistic logic. J. Symb. Logic 62(2), 529–544 (1997) · Zbl 0887.03002 [26] Kripke S.: A completeness theorem in modal logic. J. Symb. Logic 24(1), 1–14 (1959) · Zbl 0091.00902 [27] Muskens, R.: Higher order modal logic. In: Blackburn, P., van Benthem, J.F.A.K., Wolter, F. (eds.) Handbook of Modal Logic, vol. 3 (Studies in Logic and Practical Reasoning). Elsevier, New York (2006) [28] Muskens R.: Intensional models for the theory of types. J. Symb. Logic 72(1), 98–118 (2007) · Zbl 1116.03008 [29] Nipkow T., Paulson L.C., Wenzel M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer, Berlin (2002) · Zbl 0994.68131 [30] Slind K., Norrish M.: A brief overview of HOL4. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds) Theorem Proving in Higher Order Logics, TPHOLs 2008, LNCS, vol. 5170, pp. 28–32. Springer, Berlin (2008) · Zbl 1165.68474
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.