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 proceedingConference contributionpeer-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 languageEnglish
Title of host publicationComputer Science - Theory and Applications - 10th International Computer Science Symposium in Russia, CSR 2015, Proceedings
EditorsLev D. Beklemishev, Daniil V. Musatov, Daniil V. Musatov
PublisherSpringer Verlag
Pages398-411
Number of pages14
ISBN (Print)9783319202969
DOIs
Publication statusPublished - 2015
Externally publishedYes
Event10th International Computer Science Symposium in Russia, CSR 2015 - Listvyanka, Russian Federation
Duration: 13 Jul 201517 Jul 2015

Publication series

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

Conference

Conference10th International Computer Science Symposium in Russia, CSR 2015
Country/TerritoryRussian Federation
CityListvyanka
Period13/07/1517/07/15

Fingerprint

Dive into the research topics of 'Interacting with modal logics in the Coq proof assistant'. Together they form a unique fingerprint.

Cite this