package coq-comp-dec-modal

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.