This project presents machine-checked constructive proofs of soundness, completeness, decidability, and the small-model property for the logics K, K*, CTL, and PDL (with and without converse).

For all considered logics, we prove soundness and completeness of their respective Hilbert-style axiomatization. For K, K*, and CTL, we also prove soundness and completeness for Gentzen systems (i.e., sequent calculi).

For each logic, the central construction is a pruning-based algorithm computing for a given formula either a satisfying model of bounded size or a proof of its negation. The completeness and decidability results then follow with soundness from the existence of said algorithm.

• Author(s):
  • Christian Doczkal (initial)
• Coq-community maintainer(s):
  • Christian Doczkal (@chdoc)
• License: CeCILL-B
• Compatible Coq versions: 8.16 or later
• Additional dependencies:
  • MathComp 2.0 or later (ssreflect suffices)
  • Hierarchy Builder 1.6.0 or later
• Coq namespace: CompDecModal
• Related publication(s):
  • A Machine-Checked Constructive Metatheory of Computation Tree Logic doi:10.22028/D291-26649
  • Completeness and decidability of converse PDL in the constructive type theory of Coq doi:10.1145/3167088

The easiest way to install the latest released version of Completeness and Decidability of Modal Logic Calculi is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-comp-dec-modal

To instead build and install manually, do:

git clone https://github.com/coq-community/comp-dec-modal.git
cd comp-dec-modal
make   # or make -j <number-of-cores-on-your-machine> 
make install

The developments for the individual logics are described in the publications listed above. The developments on K, K*, and CTL are described in the author's PhD thesis titled "A Machine-Checked Constructive Metatheory of Computation Tree Logic". The developments on PDL and PDL with converse are described in the CPP'18 paper.

• The directory libs contains infrastructure shared between the developments. This includes:
  • fset.v: a library for finite sets over types with a choice operator (a precursor of finmap).
  • fset_tac.v: rudimentary automation for the above (originally implemented by Alexander Anisimov).
  • modular_hilbert.v: a library for constructing proofs in Hilbert axiomatizations for modal logics.
  • sltype.v: generic lemmas for alpha/beta decomposition of modal-logic formulas.
• the remaining directories contain the formalizations for the respective logics.