License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2019.31
URN: urn:nbn:de:0030-drops-110866
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11086/
Go to the corresponding LIPIcs Volume Portal

Wu, Minchao ; Goré, Rajeev

Verified Decision Procedures for Modal Logics

pdf-format:
LIPIcs-ITP-2019-31.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{wu_et_al:LIPIcs:2019:11086,
  author =	{Minchao Wu and Rajeev Gor{\'e}},
  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 =	{John Harrison and John O'Leary and Andrew Tolmach},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/11086},
  URN =		{urn:nbn:de:0030-drops-110866},
  doi =		{10.4230/LIPIcs.ITP.2019.31},
  annote =	{Keywords: Formal Methods, Interactive Theorem Proving, Modal Logic, Lean}
}

Keywords: Formal Methods, Interactive Theorem Proving, Modal Logic, Lean
Collection: 10th International Conference on Interactive Theorem Proving (ITP 2019)
Issue Date: 2019
Date of publication: 05.09.2019
Supplementary Material: The formalization is available at https://github.com/minchaowu/ModalTab

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI