Document Open Access Logo

Verified Decision Procedures for Modal Logics

Authors Minchao Wu , Rajeev Goré

Thumbnail PDF


  • Filesize: 499 kB
  • 19 pages

Document Identifiers

Author Details

Minchao Wu
  • Research School of Computer Science, Australian National University, Australia
Rajeev Goré
  • Research School of Computer Science, Australian National University, Australia

Cite AsGet BibTex

Minchao Wu and Rajeev Goré. Verified Decision Procedures for Modal Logics. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 31:1-31:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)


We describe a formalization of modal tableaux with histories for the modal logics K, KT and S4 in Lean. We describe how we formalized the static and transitional rules, the non-trivial termination and the correctness of loop-checks. The formalized tableaux are essentially executable decision procedures with soundness and completeness proved. Termination is also proved in order to define them as functions in Lean. All of these decision procedures return a concrete Kripke model in cases where the input set of formulas is satisfiable, and a proof constructed via the tableau rules witnessing unsatisfiability otherwise. We also describe an extensible formalization of backjumping and its verified implementation for the modal logic K. As far as we know, these are the first verified decision procedures for these modal logics.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Type theory
  • Software and its engineering → Formal methods
  • Formal Methods
  • Interactive Theorem Proving
  • Modal Logic
  • Lean


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail