Publication details
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
@INPROCEEDINGS{DoczkalBard,
title = {Completeness and decidability of converse PDL in the constructive type theory of Coq},
author = {Christian Doczkal and Joachim Bard},
year = {2018},
publisher = {ACM},
booktitle = {7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, USA, January 8-9, 2018},
pages = {42--52},
address = {New York, NY, USA},
}
Login to edit
Legal notice, Privacy policy
