# Publication details

##
A Machine-Checked Constructive Metatheory of Computation Tree Logic

Christian Doczkal

PhD Thesis, Saarland University, March 2016

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. We base our proofs 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.

Coq Development

Download PDF
Show BibTeX

@PHDTHESIS{Doczkal:2016:PhDThesis,
title = {A Machine-Checked Constructive Metatheory of Computation Tree Logic},
author = {Christian Doczkal},
year = {2016},
month = {Mar},
school = {Saarland University},
}

Login to edit

Legal notice, Privacy policy