Interacting with Modal Logics in the Coq Proof Assistant
From MaRDI portal
Publication:3194730
DOI10.1007/978-3-319-20297-6_25zbMath1465.03051OpenAlexW340252736MaRDI QIDQ3194730
Bruno Woltzenlogel Paleo, Christoph Benzmüller
Publication date: 20 October 2015
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-20297-6_25
Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35) Formalization of mathematics in connection with theorem provers (68V20)
Related Items (25)
Variants of Gödel's ontological proof in a natural deduction calculus ⋮ Algebraic Investigation of Connected Components ⋮ Reasoning About Cardinalities of Relations with Applications Supported by Proof Assistants ⋮ Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics ⋮ Resource operators for \(\lambda\)-calculus ⋮ \textsf{LOGIC}: a Coq library for logics ⋮ An extensible equality checking algorithm for dependent type theories ⋮ Arctic Termination ...Below Zero ⋮ Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument ⋮ Para-Disagreement Logics and Their Implementation Through Embedding in Coq and SMT ⋮ Partiality, State and Dependent Types ⋮ Injective types in univalent mathematics ⋮ Correct Code Containing Containers ⋮ Certification of Proving Termination of Term Rewriting by Matrix Interpretations ⋮ Sawja: Static Analysis Workshop for Java ⋮ Certified Reasoning with Infinity ⋮ Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions ⋮ Certifying Findel derivatives for blockchain ⋮ N. G. de Bruijn's contribution to the formalization of mathematics ⋮ Exercising Nuprl’s Open-Endedness ⋮ Axiomatic and dual systems for constructive necessity, a formally verified equivalence ⋮ Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience ⋮ Proof Documents for Automated Origami Theorem Proving ⋮ A general proof certification framework for modal logic ⋮ Formally computing with the non-computable
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Types, tableaus, and Gödel's God
- Isabelle/HOL. A proof assistant for higher-order logic
- Quantified multimodal logics in simple type theory
- Satallax: An Automatic Higher-Order Prover
- HOL Light: An Overview
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- Higher-order semantics and extensionality
This page was built for publication: Interacting with Modal Logics in the Coq Proof Assistant
