DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2019.31

Verified Decision Procedures for Modal Logics

Authors: Minchao Wu and Rajeev Goré

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{wu_et_al:LIPIcs.ITP.2019.31,
  author =	{Wu, Minchao and Gor\'{e}, Rajeev},
  title =	{{Verified Decision Procedures for Modal Logics}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{31:1--31:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.31},
  URN =		{urn:nbn:de:0030-drops-110866},
  doi =		{10.4230/LIPIcs.ITP.2019.31},
  annote =	{Keywords: Formal Methods, Interactive Theorem Proving, Modal Logic, Lean}
}

Search Results

Documents authored by Wu, Minchao

Verified Decision Procedures for Modal Logics

Abstract

Cite as

Thanks for your feedback!

Could not send message