zbMATH — the first resource for mathematics

Higher-order modal logics: automation and applications. (English) Zbl 1358.68273
Faber, Wolfgang (ed.) et al., Reasoning web. Web logic rules. 11th international summer school 2015, Berlin, Germany, July 31 – August 4, 2015. Tutorial lectures. Cham: Springer (ISBN 978-3-319-21767-3/pbk; 978-3-319-21768-0/ebook). Lecture Notes in Computer Science 9203, 32-74 (2015).
Summary: These are the lecture notes of a tutorial on higher-order modal logics held at the 11th Reasoning Web Summer School. After defining the syntax and (possible worlds) semantics of some higher-order modal logics, we show that they can be embedded into classical higher-order logic by systematically lifting the types of propositions, making them depend on a new atomic type for possible worlds. This approach allows several well-established automated and interactive reasoning tools for classical higher-order logic to be applied also to modal higher-order logic problems. Moreover, also meta reasoning about the embedded modal logics becomes possible. Finally, we illustrate how our approach can be useful for reasoning with web logics and expressive ontologies, and we also sketch a possible solution for handling inconsistent data.
For the entire collection see [Zbl 1358.68011].

68T27 Logic in artificial intelligence
03B35 Mechanization of proofs and logical operations
03B45 Modal logic (including the logic of norms)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI
[1] Web semantics: Science, services and agents on the world wide web, special issue on reasoning with context in the semantic web, vol. 12–13, pp. 1–160 (2012)
[2] Adams, R.M.: Introductory Note to *1970. In: Feferman, S., et al. (eds.) Kurt Gödel, Collected Works, vol. III. Oxford University Press, New York (1995)
[3] Akman, V., Surav, M.: Steps toward formalizing context. AI Mag. 17(3), 55–72 (1996)
[4] Alama, J., Heskes, T., Kühlwein, D., Tsivtsivadze, E., Urban, J.: Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reasoning 52(2), 191–213 (2014) · Zbl 1315.68217 · doi:10.1007/s10817-013-9286-5
[5] Anderson, A.C., Gettings, M.: Gödel’s ontological proof revisited. In: Hájek, P. (ed.) Gödel ’96: Logical foundations of mathematics, computer science and physics. Lecture Notes in Logic, vol. 6, pp. 167–172. Springer, Berlin (1996) · Zbl 0855.03005 · doi:10.1007/978-3-662-21963-8_10
[6] Andrews, P.B.: General models and extensionality. J. Symb. Logic 37(2), 395–397 (1972) · Zbl 0264.02050 · doi:10.2307/2272982
[7] Andrews, P.B.: Church’s type theory. In: Zalta, E.N. (ed.), The Stanford Encyclopedia of Philosophy. Spring 2014 edition, 2014
[8] Andrews, P.B., Miller, D.A.: Eve Longini Cohen, and Frank Pfenning. Automating higher-order logic. In: Bledsoe, W.W., Loveland, D.W., et al., Automated Theorem Proving: After 25 Years, vol. 29 of Contemporary Mathematics series, pp. 169–192. American Mathematical Society (1984)
[9] Andrews, P.B., Bishop, M.: On sets, types, fixed points, and checkerboards. In: Miglioli, P., Moscato, U., Mundici, D., Ornaghi, D. (eds.) Theorem Proving with Analytic Tableaux and Related Methods. LNCS, vol. 1071, pp. 1–15. Springer, Heidelberg (1996)
[10] Marcos, J.: Modality and paraconsistency. The Logica Yearbook, pp. 213–222 (2005)
[11] Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, New York (2003) · Zbl 1058.68107
[12] Benzmüller, C., Theiss, F., Paulson, L., Fietzke, A.: LEO-II - a cooperative automatic theorem prover for higher-order logic. In: Proceedings of IJCAR 2008, number 5195 in LNAI, pp. 162–170. Springer, Berlin (2008) · Zbl 1165.68446
[13] Benzmüller, C., Woltzenlogel Paleo, B.: Formalization, Mechanization and Automation of Gödel’s Proof of God’s Existence. arXiv: 1308.4526 (2013)
[14] Benzmüller, C.: Verifying the modal logic cube is an easy task (for higher-order automated reasoners). In: Siegler, S., Wasser, N. (eds.) Walther Festschrift. LNCS, vol. 6463, pp. 117–128. Springer, Heidelberg (2010) · Zbl 1309.68166 · doi:10.1007/978-3-642-17172-7_7
[15] Benzmüller, C., Brown, C.: The curious inference of Boolos in MIZAR and OMEGA. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof - Festschrift in Honour of Andrzej Trybulec. Studies in Logic, Grammar, and Rhetoric, vol. 10(23), pp. 299–388. The University of Bialystok, Polen (2007)
[16] Benzmüller, C., Brown, C.E., Kohlhase, M.: Higher-order semantics and extensionality. J. Symb. Logic 69(4), 1027–1088 (2004) · Zbl 1071.03024 · doi:10.2178/jsl/1102022211
[17] Benzmüller, C., Otten, J., Raths, T.: Implementing and evaluating provers for first-order modal logics. In: Raedt, L.D., Bessiere, C., Dubois, D., Doherty, P., Frasconi, P., Heintz, F., Lucas, P. (eds.), ECAI 2012, Frontiers in Artificial Intelligence and Applications, vol. 242, pp. 163–168. IOS Press, Montpellier (2012) · Zbl 1327.68204
[18] Benzmüller, C., Woltzenlogel Paleo, B.: Gödel’s God in Isabelle/HOL. Arch. Formal Proofs, 2013 (2013) · Zbl 06545645
[19] Benzmüller, C., Woltzenlogel Paleo, B.: Automating Gödel’s ontological proof of God’s existence with higher-order automated theorem provers. In: Schaub, T., Friedrich, G., O’Sullivan, B., (eds.), ECAI 2014, Frontiers in Artificial Intelligence and Applications, vol. 263, pp. 93–98, IOS Press (2014) · Zbl 1366.03169
[20] Benzmüller, C., Paulson, L.: Exploring properties of normal multimodal logics in simple type theory with LEO-II. In: Benzmüller, C., Brown, C., Siekmann, J., Statman, R. (eds.), Reasoning in Simple Type Theory – Festschrift in Honor of Peter B. Andrews on His 70th Birthday, Studies in Logic, Mathematical Logic and Foundations, pp. 386–406, College Publications (2008) · Zbl 1227.03017
[21] Benzmüller, C., Paulson, L.: Quantified multimodal logics in simple type theory. Logic Univers. (Spec. Issue Multimodal Logics) 7(1), 7–20 (2013) · Zbl 1334.03014 · doi:10.1007/s11787-012-0052-y
[22] Benzmüller, C., Pease, A.: Higher-order aspects and context in SUMO. J. Web Seman. (Spec. Issue Reasoning with context in the Semant. Web) 12–13, 104–117 (2012)
[23] Benzmüller, Christoph, Raths, Thomas: HOL based first-order modal logic provers. In: McMillan, Ken, Middeldorp, Aart, Voronkov, Andrei (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 127–136. Springer, Heidelberg (2013) · Zbl 1406.68103 · doi:10.1007/978-3-642-45221-5_9
[24] Benzmüller, C., Weber, L., Woltzenlogel Paleo, B.: Computer-assisted analysis of the Anderson-Hájek ontological controversy. In: Silvestre, R.S., Béziau, J.-Y. (eds.), Handbook of the 1st World Congress on Logic and Religion, Joao Pessoa, Brasil (2015) · Zbl 1417.03131
[25] Beziau, J.Y., Carnielli, W., Gabbay, D.: Handbook of Paraconsistency. College Publications, London (2007)
[26] Blackburn, P., van Benthem, J.F.A.K., Wolter, F.: Handbook of Modal Logic, Volume 3 (Studies in Logic and Practical Reasoning). Elsevier Science Inc., New York (2006) · Zbl 1114.03001
[27] Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. J. Autom. Reasoning 51(1), 109–128 (2013) · Zbl 1314.68272 · doi:10.1007/s10817-013-9278-5
[28] Blanchette, Jasmin Christian, Nipkow, Tobias: Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, Matt, Paulson, Lawrence C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131–146. Springer, Heidelberg (2010) · Zbl 1291.68326 · doi:10.1007/978-3-642-14052-5_11
[29] Boolos, G.: A curious inference. J. Philos. Logic 16, 1–12 (1987) · Zbl 0623.03054 · doi:10.1007/BF00250612
[30] Brown, C.E.: Satallax: An automated higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Automated Reasoning. LNCS, vol. 7364, pp. 111–117. Springer, Heidelberg (2012) · Zbl 1358.68250 · doi:10.1007/978-3-642-31365-3_11
[31] Bucav, S., Buvac, V., Mason, I.A.: Metamathematics of contexts. Fundamenta Informaticae 23(3), 263–301 (1995)
[32] Charguéraud, A.: The locally nameless representation. J. Autom. Reasoning 49(3), 363–408 (2012) · Zbl 1260.68368 · doi:10.1007/s10817-011-9225-2
[33] Corazzon, R.: Contemporary bibliography on ontological arguments. http://www.ontology.co/biblio/ontological-proof-contemporary-biblio.htm
[34] da Costa, N.C.A., Alves, E.H.: Semantical analysis of the calculi cn. Notre Dame J. Formal Logic 18(4), 621–630 (1977) · Zbl 0349.02022 · doi:10.1305/ndjfl/1093888132
[35] Dunn, J.M., Restall, G.: Relevance logic. Handbook of Philosophical Logic 6, 1–136 (2002) · doi:10.1007/978-94-017-0460-1_1
[36] Fitting, M.: Types, Tableaux and Gödel’s God, Kluwer (2002) · Zbl 1038.03001 · doi:10.1007/978-94-010-0411-4
[37] Fitting, M., Mendelsohn, R.L.: First-Order Modal Logic. Synthese Library. Kluwer, Netherlands (1998) · Zbl 1025.03001 · doi:10.1007/978-94-011-5292-1
[38] Gabbay, D.M.: Labelled Deductive Systems. Clarendon Press, Oxford (1996) · Zbl 0858.03004
[39] Gallin, D.: Intensional and Higher-Order Modal Logic. North Holland, New York (1975) · Zbl 0341.02014
[40] Giunchiglia, F.: Contextual reasoning. Epistemologia (Special Issue on Languages and Machines) 16, 345–364 (1993)
[41] Giunchiglia, F., Serafini, L.: Multilanguage hierarchical logics or: How we can do without modal logics. Artif. Intell. 65(1), 29–70 (1994) · Zbl 0787.68093 · doi:10.1016/0004-3702(94)90037-X
[42] Gödel, K.: Collected Works, Unpublished Essays and Letters. Ontological Proof, pp. 65–85. Oxford University Press, Oxford (1970)
[43] Gödel, K.: Appx.A: Notes in Kurt Gödel’s Hand. In: [70], pp. 144–145 (2004)
[44] Guha, R.V.: Context: A Formalization and Some Applications. Ph.D. thesis, Stanford University (1991)
[45] Henkin, L.: Completeness in the theory of types. J. Symb. Logic 15(2), 81–91 (1950) · Zbl 0039.00801 · doi:10.2307/2266967
[46] Jaśkowski, S.: Rachunek zdań dla systemów dedukcyjnych sprzecznych. Stud. Soc. Scientiarun Torunesis 1(5), 55–77 (1948)
[47] Jaśkowski, S.: Propositional calculus for contradictory deductive systems. Stud. Logica. 24, 143–157 (1969) · Zbl 0244.02004 · doi:10.1007/BF02134311
[48] Kaliszyk, C., Urban, J.: Hol(y)hammer: online ATP service for HOL light. Math. Comput. Sci. 9(1), 5–22 (2015) · Zbl 1322.68177 · doi:10.1007/s11786-014-0182-0
[49] Kaliszyk, C., Urban, J.: Learning-assisted theorem proving with millions of lemmas. J. Symb. Comput. 69, 109–128 (2015) · Zbl 1315.68220 · doi:10.1016/j.jsc.2014.09.032
[50] Lindblad, F.: agsyHOL website. https://github.com/frelindb/agsyHOL
[51] McCarthy, J.: Generality in artificial intelligence. Commun. ACM 30(12), 1030–1035 (1987) · Zbl 0644.68004 · doi:10.1145/33447.33448
[52] McCarthy, J.: Notes on formalizing context. In: Proceedings of IJCAI 1993, pp. 555–562 (1993)
[53] Muskens, R.: Higher order modal logic. In: Blackburn, P., et al. (eds.) Handbook of Modal Logic, pp. 621–653. Elsevier, Dordrecht (2006)
[54] 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 · doi:10.1007/3-540-45949-9
[55] Otten, J.: Mleancop: A connection prover for first-order modal logic. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) Automated Reasoning. LNCS, vol. 8562, pp. 269–276. Springer, Switzerland (2014) · Zbl 1423.68423 · doi:10.1007/978-3-319-08587-6_20
[56] Woltzenlogel Paleo, B., Benzmüller, C.: Formal theology repository. ( https://github.com/FormalTheology/GoedelGod )
[57] Paulin-Mohring, C.: Introduction to the calculus of inductive constructions. In: Delahaye, D., Woltzenlogel Paleo, B. (eds.), All about Proofs, Proofs for All, Mathematical Logic and Foundations. College Publications, London (2015)
[58] Pease, A.: Ontology: A Practical Guide. Articulate Software Press, Angwin (2011)
[59] Pease, A., Sutcliffe, G.: First order reasoning on a large ontology. In: Sutcliffe, G., Urban, J., Schulz, S. (eds.), Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories (ESARLT), CEUR Workshop Proceedings, vol. 257, CEUR-WS.org (2007)
[60] Priest, G.: Paraconsistent belief revision. Theoria 67, 214–228 (2001) · doi:10.1111/j.1755-2567.2001.tb00204.x
[61] Priest, G., Sylvan, R.: Simplified semantics for basic relevant logics. J. Philos. Logic (1992) · Zbl 0782.03008 · doi:10.1007/BF00248640
[62] Ramachandran, D., Reagan, P., Goolsbey, K.: First-orderized ResearchCyc: Expressivity and efficiency in a common-sense ontology. In: Shvaiko P. (ed.), Papers from the AAAI Workshop on Contexts and Ontologies: Theory, Practice and Applications, Pittsburgh, Pennsylvania, USA, 2005. Technical report WS-05-01 published by The AAAI Press, Menlo Park, California, July 2005
[63] Raths, Thomas, Otten, Jens: The QMLTP problem library for first-order modal logics. In: Gramlich, Bernhard, Miller, Dale, Sattler, Uli (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 454–461. Springer, Heidelberg (2012) · Zbl 1358.68262 · doi:10.1007/978-3-642-31365-3_35
[64] Restall, G., Slaney, J.: Realistic belief revision. In: Proceedings of the Second World Conference in the Fundamentals of Artificial Intelligence, pp. 367–378 (1995)
[65] Scott, D.: Appx.B: Notes in Dana Scott’s Hand. In: [70], pp. 145–146 (2004)
[66] Serafini, L., Bouquet, P.: Comparing formal theories of context in AI. Artif. Intell. 155, 41–67 (2004) · Zbl 1085.68164 · doi:10.1016/j.artint.2003.11.001
[67] Siders, A., Woltzenlogel Paleo, B.: A variant of Gödel’s ontological proof in a natural deduction calculus. ( github.com/FormalTheology/GoedelGod/blob/master/Papers/InProgress/NaturalDeduction/GodProof-ND.pdf?raw=true )
[68] Sobel, J.H.: Gödel’s ontological proof. In On Being and Saying. Essays for Richard Cartwright, pp. 241–261, MIT Press (1987)
[69] Sobel, J.H.: Logic and Theism: Arguments for and Against Beliefs in God. Cambridge University Press, Cambridge (2004)
[70] Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reasoning 43(4), 337–362 (2009) · Zbl 1185.68636 · doi:10.1007/s10817-009-9143-8
[71] Sutcliffe, G., Benzmüller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Formalized Reasoning 3(1), 1–27 (2010) · Zbl 1211.68371
[72] Tanaka, K.: Three schools of paraconsistency. The Australas. J. Logic 1, 28–42 (2003) · Zbl 1038.03007
[73] Wenzel, M.: Hoare logic in isabelle. http://isabelle.in.tum.de/dist/library/HOL/HOL-Isar_Examples/Hoare.html · Zbl 1166.68337
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.