Publication details
Constructive Completeness for Modal Logic with Transitive Closure
Christian Doczkal, Gert Smolka
Certified Programs and Proofs, Second International Conference (CPP 2012), Vol. 7679 of LNCS, pp. 224-239, Springer, 2012
Classical modal logic with transitive closure appears as a subsystem of logics used for program verification. The logic can be axiomatized with a Hilbert system. In this paper we develop a constructive completeness proof for the axiomatization using Coq with Ssreflect. The proof is based on a novel analytic Gentzen system, which yields a certifying decision procedure that for a formula constructs either a derivation or a finite countermodel. Completeness of the axiomatization then follows by translating Gentzen derivations to Hilbert derivations. The main difficulty throughout the development is the treatment of transitive closure.
Coq Development
Download PDF
Show BibTeX
@INPROCEEDINGS{DoczkalSmolka:2012:ContructiveTC,
title = {Constructive Completeness for Modal Logic with Transitive Closure},
author = {Christian Doczkal and Gert Smolka},
year = {2012},
editor = {Chris Hawblitzel and Dale Miller},
publisher = {Springer},
booktitle = {Certified Programs and Proofs, Second International Conference (CPP 2012)},
series = {LNCS},
volume = {7679},
pages = {224-239},
}
Login to edit
Legal notice, Privacy policy
