zbMATH — the first resource for mathematics

Interacting with modal logics in the coq proof assistant. (English) Zbl 06496834
Beklemishev, Lev D. (ed.) et al., Computer science – theory and applications. 10th international computer science symposium in Russia, CSR 2015, Listvyanka, Russia, July 13–17, 2015. Proceedings. Cham: Springer (ISBN 978-3-319-20296-9/pbk; 978-3-319-20297-6/ebook). Lecture Notes in Computer Science 9139, 398-411 (2015).
Summary: This paper describes an embedding of higher-order modal logics in the Coq proof assistant. Coq’s capabilities are used to implement modal logics in a minimalistic manner, which is nevertheless sufficient for the formalization of significant, non-trivial modal logic proofs. The elegance, flexibility and convenience of this approach, from a user perspective, are illustrated here with the successful formalization of Gödel’s ontological argument.
For the entire collection see [Zbl 1316.68003].

68Qxx Theory of computing
Full Text: DOI
[1] Benzmüller, C., Paleo, B.W.: Formalization, mechanization and automation of Gödel’s proof of god’s existence. CoRR, abs/1308.4526 (2013)
[2] Benzmüller, C., Paleo, B.W.: Gödel’s God inIsabelle/HOL. Archive of Formal Proofs, 2013 (2013)
[3] Benzmüller, C., Paulson, L.C.: Exploring properties of normal multimodal logics in simple type theory with LEO-II. In: Festschrift in Honor of Peter B. Andrews on His 70th Birthday, pp. 386-406. College Publications (2008) · Zbl 1227.03017
[4] Benzmüller, C., Paulson, L.C.: Quantified multimodal logics in simple type theory. Logica Universalis (Special Issue on Multimodal Logics) 7(1), 7-20 (2013) · Zbl 1334.03014 · doi:10.1007/s11787-012-0052-y
[5] Benzmüller, C.E., Paulson, L.C., Theiss, F., Fietzke, A.: LEO-II - a cooperative automatic theorem prover for classical higher-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 162-170. Springer, Heidelberg (2008) · Zbl 1165.68446 · doi:10.1007/978-3-540-71070-7_14
[6] Benzmüller, C., Brown, C.E., Kohlhase, M.: Higher-order semantics and extensionality. J. Symb. Log. 69(4), 1027-1088 (2004) · Zbl 1071.03024 · doi:10.2178/jsl/1102022211
[7] Benzmüller, C., Otten, J., Raths, T.: Implementing and evaluating provers for first-order modal logics. In: ECAI 2012-20th European Conference on Artificial Intelligence, pp. 163-168 (2012) · Zbl 1327.68204
[8] Blackburn, P., Benthem, J.v., Wolter, F.: Handbook of Modal Logic. Elsevier, Amsterdam (2006) · Zbl 1114.03001
[9] Brown, C.E.: Satallax: an automatic higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 111-117. Springer, Heidelberg (2012) · Zbl 1358.68250 · doi:10.1007/978-3-642-31365-3_11
[10] Corazzon, R.: Contemporary bibliography on the ontological proof. (
[11] Fitting, M.: Types, Tableaux and Gödel’s God. Kluver Academic Press, Dordrecht (2002) · Zbl 1038.03001
[12] Gabbay, D.M.: Labelled Deductive Systems. Clarendon Press, Oxford (1996) · Zbl 0858.03004
[13] Gödel, K.: Ontological proof. In: Gödel, K.: Collected Works, Unpublished Essays and Letters. vol. 3, pp. 403-404. Oxford University Press, Oxford (1970)
[14] Harrison, J.: HOL light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 60-66. Springer, Heidelberg (2009) · Zbl 1252.68255 · doi:10.1007/978-3-642-03359-9_4
[15] Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002) · Zbl 0994.68131
[16] Oppenheimer, P.E., Zalta, E.N.: A computationally-discovered simplification of the ontological argument. Australas. J. Philos. 2(89), 333-349 (2011) · doi:10.1080/00048401003674482
[17] Paleo, B.W., Benzmüller, C.: Formal theology repository. (
[18] Paulin-Mohring, C.: Introduction to the calculus of inductive constructions. In: Delahaye, D., Paleo, B.W. (eds.) All about Proofs, Proofs for All. Mathematical Logic and Foundations. College Publications, London (2015)
[19] Rushby, J.: The ontological argument in PVS. In: Proceedings of CAV Workshop Fun With Formal Methods, St. Petersburg, Russia (2013)
[20] Schmidt, R.: List of modal provers. (
[21] Scott, D.: Appendix B. Notes in Dana Scott’s hand. In: [24] (2004)
[22] Siders, A., Paleo, B.W.: A variant of Gödel’s ontological proof in a natural deduction calculus. (
[23] Sobel, J.H.: Gödel’s ontological proof. In: On Being and Saying. Essays for Richard Cartwright, pp. 241-261. MIT Press, Cambridge (1987)
[24] Sobel, J.H.: Logic and Theism: Arguments for and Against Beliefs in God. Cambridge University Press, Cambridge (2004)
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.