Verified Tableaux: from Modal Logics to Modal Fixpoint Logics

Abstract We formalise tableau procedures for the modal logics K, KT, and S4, and the modal fixpoint logic LTL, in the proof assistant Coq version 8.17.1. This involves encoding the algorithms, and formally proving their termination and their correctness, the latter boiling down to showing that they are both sound and complete with respect to the semantics of these logics. We give a quick overview of our account of S4 because most of the work had already been achieved by Wu and Goré then focus on LTL: we describe the rules of our tableau calculus and our approach to formally verify it in Coq. Unlike K and KT, these logics require checking for loops and need particular attention to build a satisfying model. Moreover, for LTL, we must also distinguish “good loops” from “bad loops” due to the presence of least and greatest fixpoint modalities. We show how we manage to implement loop-checks to ensure termination and how a model can be constructed from their tableau tree in order to prove soundness. We also demonstrate how the eventuality formulae of LTL are handled in the tableau rules and the various proofs. Such algorithms encoded in Coq can easily be modified to output a satisfying model in the case where the input is satisfiable. We use the program extraction feature of Coq to produce source code for the verified tableau procedures in OCaml and compile them to obtain actual executable programs. We then evaluate these verified programs on the standard benchmarks against other reasoners which are optimised but unverified. As expected, the results show a clear inferiority of our verified reasoners in terms of efficiency, however they still demonstrate that we can be optimistic regarding the usability of verified reasoners in practice. Wu, M., Goré, R.: Verified decision procedures for modal logics.