Joachim Bard

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

2017

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 …