Interacting with modal logics in the Coq proof assistant

Christoph Benzmüller; Bruno Woltzenlogel Paleo

doi:10.1007/978-3-319-20297-6_25

Interacting with modal logics in the Coq proof assistant

Christoph Benzmüller, Bruno Woltzenlogel Paleo^*

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

20 Citations (Scopus)

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.

Original language	English
Title of host publication	Computer Science - Theory and Applications - 10th International Computer Science Symposium in Russia, CSR 2015, Proceedings
Editors	Lev D. Beklemishev, Daniil V. Musatov, Daniil V. Musatov
Publisher	Springer Verlag
Pages	398-411
Number of pages	14
ISBN (Print)	9783319202969
DOIs	https://doi.org/10.1007/978-3-319-20297-6_25
Publication status	Published - 2015
Externally published	Yes
Event	10th International Computer Science Symposium in Russia, CSR 2015 - Listvyanka, Russian Federation Duration: 13 Jul 2015 → 17 Jul 2015

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	9139
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	10th International Computer Science Symposium in Russia, CSR 2015
Country/Territory	Russian Federation
City	Listvyanka
Period	13/07/15 → 17/07/15

Access to Document

10.1007/978-3-319-20297-6_25

Cite this

Benzmüller, C., & Paleo, B. W. (2015). Interacting with modal logics in the Coq proof assistant. In L. D. Beklemishev, D. V. Musatov, & D. V. Musatov (Eds.), Computer Science - Theory and Applications - 10th International Computer Science Symposium in Russia, CSR 2015, Proceedings (pp. 398-411). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9139). Springer Verlag. https://doi.org/10.1007/978-3-319-20297-6_25

Benzmüller, Christoph ; Paleo, Bruno Woltzenlogel. / Interacting with modal logics in the Coq proof assistant. Computer Science - Theory and Applications - 10th International Computer Science Symposium in Russia, CSR 2015, Proceedings. editor / Lev D. Beklemishev ; Daniil V. Musatov ; Daniil V. Musatov. Springer Verlag, 2015. pp. 398-411 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{324fc16495d54f17a6a8822b33be0d5a,

title = "Interacting with modal logics in the Coq proof assistant",

abstract = "This paper describes an embedding of higher-order modal logics in the Coq proof assistant. Coq{\textquoteright}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{\"o}del{\textquoteright}s ontological argument.",

author = "Christoph Benzm{\"u}ller and Paleo, {Bruno Woltzenlogel}",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2015.; 10th International Computer Science Symposium in Russia, CSR 2015 ; Conference date: 13-07-2015 Through 17-07-2015",

year = "2015",

doi = "10.1007/978-3-319-20297-6_25",

language = "English",

isbn = "9783319202969",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "398--411",

editor = "Beklemishev, {Lev D.} and Musatov, {Daniil V.} and Musatov, {Daniil V.}",

booktitle = "Computer Science - Theory and Applications - 10th International Computer Science Symposium in Russia, CSR 2015, Proceedings",

address = "Germany",

}

Benzmüller, C & Paleo, BW 2015, Interacting with modal logics in the Coq proof assistant. in LD Beklemishev, DV Musatov & DV Musatov (eds), Computer Science - Theory and Applications - 10th International Computer Science Symposium in Russia, CSR 2015, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9139, Springer Verlag, pp. 398-411, 10th International Computer Science Symposium in Russia, CSR 2015, Listvyanka, Russian Federation, 13/07/15. https://doi.org/10.1007/978-3-319-20297-6_25

Interacting with modal logics in the Coq proof assistant. / Benzmüller, Christoph; Paleo, Bruno Woltzenlogel.
Computer Science - Theory and Applications - 10th International Computer Science Symposium in Russia, CSR 2015, Proceedings. ed. / Lev D. Beklemishev; Daniil V. Musatov; Daniil V. Musatov. Springer Verlag, 2015. p. 398-411 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9139).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Interacting with modal logics in the Coq proof assistant

AU - Benzmüller, Christoph

AU - Paleo, Bruno Woltzenlogel

N1 - Publisher Copyright: © Springer International Publishing Switzerland 2015.

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84950132612&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-20297-6_25

DO - 10.1007/978-3-319-20297-6_25

M3 - Conference contribution

AN - SCOPUS:84950132612

SN - 9783319202969

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 398

EP - 411

BT - Computer Science - Theory and Applications - 10th International Computer Science Symposium in Russia, CSR 2015, Proceedings

A2 - Beklemishev, Lev D.

A2 - Musatov, Daniil V.

PB - Springer Verlag

T2 - 10th International Computer Science Symposium in Russia, CSR 2015

Y2 - 13 July 2015 through 17 July 2015

ER -

Benzmüller C, Paleo BW. Interacting with modal logics in the Coq proof assistant. In Beklemishev LD, Musatov DV, Musatov DV, editors, Computer Science - Theory and Applications - 10th International Computer Science Symposium in Russia, CSR 2015, Proceedings. Springer Verlag. 2015. p. 398-411. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-20297-6_25

Interacting with modal logics in the Coq proof assistant

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this