Joachim Bard: Bachelor's Thesis

Saarland University Computer Science

A Formal Completeness Proof for Test-free PDL

Advisor: Christian Doczkal


In this thesis we give a formalization of test-free PDL based on results from the literature using the proof assistant Coq. We show soundness and completeness for a Hilbert system. In order to show completeness we use Hintikka sets and pruning. Pruning is a method yielding finite models for satisfiable formulas. For unsatisiable formulas pruning yields abstract refutations. We obtain completeness of the Hilbert system by translating abstract refutations to proofs in the Hilbert system. As corollaries, we also obatin the small model property, plus that satisiability, validity and Hilbert provability of a formula are decidable.



Coq Development


Joachim Bard, Fri Feb 17 15:45:40 2017