This is a library for writing modal logic proofs in the Lean programming language.

References

Code

• LEAN prover github
  • lean/library/init
• The QMLTP Library: Benchmarking Theorem Provers for First-Order Modal Logics
• "Godel's God in Isabelle/HOL (Source)"
• "Interacting with Modal Logics in the Coq Proof Assistant"
• FormalTheology/GoedelGod

Papers

• Philosophical Issues from Kripke’s ‘Semantical Considerations on Modal Logic’
• "Introduction to the Calculus of Inductive Constructions"
• "Implementing and Evaluating Provers for First-Order Modal Logics"
• "Quantified Multimodal Logics in Simple Type Theory"
• "Godel's God in Isabelle/HOL"
• "CS 3234: Logic and Formal Systems - Modal Logic"
• "Labelled Deductive Systems: A Position Paper"
• *Theorem Proving in Lean
• Lean Prover - Logic and Proof
• "Labelled Deductive Systems"
• "Systematic Verification of the Modal Logic Cube in Isabelle/HOL"
• "Steps Toward a Computational Metaphysics"