Publication details

Saarland University Computer Science

Completeness and decidability of converse PDL in the constructive type theory of Coq

Christian Doczkal, Joachim Bard

7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, USA, January 8-9, 2018, pp. 42--52, ACM, 2018

The completeness proofs for Propositional Dynamic Logic (PDL) in the literature are non-constructive and usually presented in an informal manner. We obtain a formal and constructive completeness proof for Converse PDL by recasting a completeness proof by Kozen and Parikh into our constructive setting. We base our proof on a Pratt-style decision method for satisfiability constructing finite models for satisfiable formulas and pruning refutations for unsatisfiable formulas. Completeness of Segerberg's axiomatization of PDL is then obtained by translating pruning refutations to derivations in the Hilbert system. We first treat PDL without converse and then extend the proofs to Converse PDL. All results are formalized in Coq/Ssreflect.

Link to Coq formalisation

Download PDF        Show BibTeX               

Login to edit

Legal notice, Privacy policy