Joachim Bard: Bachelor's Thesis
A Formal Completeness Proof for Test-free PDL
Advisor: Christian Doczkal
Abstract:
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.
References
-
Nondeterministic Propositional Dynamic Logic with intersection is decidable (1984)
Ryszard Danecki
-
A Machine-Checked Constructive Metatheory of Computation Tree Logic (2016)
Christian Doczkal
-
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)
Mark Kaminski
-
Dynamic Logic (2000)
David Harel, Dexter Kozen and Jerzy Tiuryn
-
A Representation Theorem for Models of *-free PDL (1980)
Dexter Kozen
-
An Elementary Proof of the Completeness of PDL (1981)
Dexter Kozen and Rohit Parikh
-
Models of Program Logics (1979)
Vaughan R. Pratt.
Thesis
-
Thesis (submitted on 1st Feb, 2017)
Coq Development
Presentations
-
Initial Seminar Talk: Slides (15th Jul, 2016)
-
Second Seminar Talk: Slides (9th Sep, 2016)
-
Final Talk: Slides (17th Feb, 2017)
Legal notice, Privacy policy
