View the project on GitHub
Welcome to the Completeness and Decidability of Modal Logic Calculi project website! This project is part of coq-community.
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.
This is an open source project, licensed under the CeCILL-B.
The current stable release of Completeness and Decidability of Modal Logic Calculi can be downloaded from GitHub.
The coqdoc presentations of the source files from releases can be browsed online.
Other related publications are listed below.