POPL 2018 (series) / CPP 2018 (series) / CPP 2018 - The 7th ACM SIGPLAN International Conference on Certified Programs and Proofs /
Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq
Mon 8 Jan 2018 11:30 - 12:00 at Museum A - Verifying Programs and Systems Chair(s): Natarajan Shankar
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.
Mon 8 JanDisplayed time zone: Tijuana, Baja California change
Mon 8 Jan
Displayed time zone: Tijuana, Baja California change
10:30 - 12:00 | |||
10:30 30mTalk | Total Haskell is Reasonable Coq CPP Antal Spector-Zabusky , Joachim Breitner University of Pennsylvania, Christine Rizkallah University of Pennsylvania, USA, Stephanie Weirich University of Pennsylvania, USA DOI | ||
11:00 30mTalk | A Formal Proof in Coq of a Control Function for the Inverted Pendulum CPP Damien Rouhling University of Côte d'Azur, France DOI | ||
11:30 30mTalk | Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq CPP DOI | ||