This project formalizes a deep embedding of arbitrary normal modal logic systems in the Coq proof assistant.
- Sets: some basic definitions for working with sets in Coq.
- Modal_Library: core of the library. This file defines the syntax of formulas, frames, models, and entailment.
- Modal_Notations: notations used throughout the development.
- Deductive_System: definition of a Hilbert-style deduction system for modal logic, quantified over a set of axioms.
- Modal_Tactics: basic auxiliary lemmas regarding derivation in the system, making it feel more natural.
- Completeness: proof of completeness in regard to the Kripke semantics.
- Frame_Validation: characterization of axioms by the kind of frame relation they represent.
- Logical_Equivalence: minor lemmas about implications on the system (this should eventually be moved).
- Soundness: proof of soundness in regard to the Kripke semantics.
- Fusion: proof for preservation of soundness through fusion of separate logic systems.
- Examples: some example derivations, including Löb's theorem.
We are aware that the files do need some cleanup. We are too tired at the moment, but we will eventually do it.
This is a research project. You may have found this code from one of our publications. The current publications about this codebase are as follow:
- A Sound Deep Embedding of Arbitrary Normal Modal Logics in Coq
- Soundness-Preserving Fusion of Modal Logics in Coq
We currently have one more paper under review; this file should be updated to reflect that after the decision is taken.
This is free software. You're free to use it under the BSD 3-clause license. Enjoy!
This project has been developed by Santa Catarina State University's research group on theoretical computer science, Função. All rights reserved.
