Publication details

Saarland University Computer Science

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               


Login to edit


Webmaster, Wed Sep 16 10:47:00 2009