Saarland University Computer Science

Constructive Completeness for Modal Logic with Transitive Closure

Christian Doczkal and Gert Smolka

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.

Paper, CPP 2012

Coq development

Coq development (Updated to compile with SSReflect 1.4)

Browse the Sources

Browse the Sources (without proofs)