Joachim Bard: Bachelor's Thesis
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.
Nondeterministic Propositional Dynamic Logic with intersection is decidable (1984)
A Machine-Checked Constructive Metatheory of Computation Tree Logic (2016)
Propositional Dynamic Logic of Regular Programs (1979)
Michael J. Fischer and Richard E. Ladner
Incremental Decision Procedures for Modal Logics with Nominals and Eventualities (2012)
Dynamic Logic (2000)
David Harel, Dexter Kozen and Jerzy Tiuryn
A Representation Theorem for Models of *-free PDL (1980)
An Elementary Proof of the Completeness of PDL (1981)
Dexter Kozen and Rohit Parikh
Models of Program Logics (1979)
Vaughan R. Pratt.
Thesis (submitted on 1st Feb, 2017)
Initial Seminar Talk: Slides (15th Jul, 2016)
Second Seminar Talk: Slides (9th Sep, 2016)
Final Talk: Slides (17th Feb, 2017)