Christian Doczkal
This thesis presents a machine-checked constructive metatheory of computation tree logic (CTL) and its sublogics K and K* based on results from the literature. We consider models, Hilbert systems, and history-based Gentzen systems and show that for every logic and every formula s the following statements are decidable and equivalent: s is true in all models, s is provable in the Hilbert system, and s is provable in the Gentzen system. Our proofs are based on pruning systems constructing finite models for satisfiable formulas and abstract refutations for unsatisfiable formulas. The pruning systems are devised such that abstract refutations can be translated to derivations in the Hilbert system and the Gentzen system, thus establishing completeness of both systems with a single model construction.
All results of this thesis are formalized and machine-checked with the Coq interactive theorem prover. Given the level of detail involved and the informal presentation in much of the original work, the gap between the original paper proofs and constructive machine-checkable proofs is considerable. The mathematical proofs presented in this thesis provide for elegant formalizations and often differ significantly from the proofs in the literature.
The formalization is carried out using Coq/Ssreflect and consists of 4 parts. In addition to the developments for the three logics K, K*, and CTL there are a number of shared libraries including a library for finite sets and a library for generating Hilbert proofs. Altogether the formalization consists of about 6800 lines code.
An updated version of the Coq development is available on GitHub
Coq Development (requires Coq-8.8.2+mathcomp-1.7, updated 2018-12-28)
Coq Development (requires Coq-8.5+mathcomp-1.6)
Below you find the HTML documentation generated from the theory files. Note: just click on an identifier to look up its definition