文章基本信息

标题：Verified Decision Procedures for Modal Logics
本地全文：下载
作者：Minchao Wu ; Rajeev Gor
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2019
卷号：141
页码：1-19
DOI：10.4230/LIPIcs.ITP.2019.31
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Formal Methods; Interactive Theorem Proving; Modal Logic; Lean