Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Propositional Proofs in Frege and Extended Frege Systems (Abstract) Kapitel lesen Erstes Kapitel lesen

2015 | OriginalPaper | Buchkapitel

Interacting with Modal Logics in the Coq Proof Assistant

verfasst von : Christoph Benzmüller, Bruno Woltzenlogel Paleo

Erschienen in: Computer Science -- Theory and Applications

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Rewriting Higher-Order Stack Trees
Nächstes Kapitel Delay Games with WMSOU Winning Conditions
Fußnoten
1
The Coq proof assistant was chosen because of the authors’ greater familiarity with the tactic language of this system. Nevertheless, the techniques presented here are likely to be useful for other proof assistants (e.g. Isabelle [15], HOL-Light [14]).
 
2
The keyword https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-20297-6_25/339533_1_En_25_IEq12_HTML.gif indicates a lambda abstraction: https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-20297-6_25/339533_1_En_25_IEq13_HTML.gif denotes the function \(\lambda x:t.p\), which takes an argument x (of type t) and returns p.
 
3
The underlying proof system of Coq (the Calculus of Inductive Constructions (CIC) [18]) is actually more sophisticated and minimalistic than the calculus shown in Fig. 1. But the calculus shown here suffices for the purposes of this paper. This calculus is classical, because of the double negation elimination rule. Although CIC is intuitionistic, it can be made classical by importing Coq ’s classical library, which adds the axiom of the excluded middle and the double negation elimination lemma.
 
4
The ND calculus with the rules from Figs. 1 and 2 is sound and complete relatively to the calculus of Fig.  1 extended with a necessitation rule and the modal axiom K [22]. Starting from a sound and Henkin-complete ND calculus for classical higher-order logic (cf. Fig. 1), the additional modal rules in Fig. 2 make it sound and Henkin-complete for the rigid higher-order modal logic K.
 
5
The proofs found automatically by the above provers indeed differ from the one presented here: e.g., the strong S5 principle used below (and by Scott) is not needed; the ATP proofs only rely on axiom B.
 
Literatur
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)
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)MATHCrossRef
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) CrossRef
6.
Benzmüller, C., Brown, C.E., Kohlhase, M.: Higher-order semantics and extensionality. J. Symb. Log. 69(4), 1027–1088 (2004)MATHCrossRef
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)
8.
Blackburn, P., Benthem, J.v., Wolter, F.: Handbook of Modal Logic. Elsevier, Amsterdam (2006)
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) CrossRef
10.
11.
Fitting, M.: Types, Tableaux and Gödel’s God. Kluver Academic Press, Dordrecht (2002)
12.
Gabbay, D.M.: Labelled Deductive Systems. Clarendon Press, Oxford (1996) MATH
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) CrossRef
15.
Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002) MATH
16.
Oppenheimer, P.E., Zalta, E.N.: A computationally-discovered simplification of the ontological argument. Australas. J. Philos. 2(89), 333–349 (2011)CrossRef
17.
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.
21.
Scott, D.: Appendix B. Notes in Dana Scott’s hand. In: [24] (2004)
22.
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)
Metadaten
Titel
Interacting with Modal Logics in the Coq Proof Assistant
verfasst von
Christoph Benzmüller
Bruno Woltzenlogel Paleo
Copyright-Jahr
2015
Buch
Computer Science -- Theory and Applications

Print ISBN: 978-3-319-20296-9

Electronic ISBN: 978-3-319-20297-6

Copyright-Jahr: 2015

DOI
https://doi.org/10.1007/978-3-319-20297-6_25