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 Jan (GMT-07:00) Tijuana, Baja California change

CPP-2018
10:30 - 12:00: CPP 2018 - Verifying Programs and Systems at Museum A
Chair(s): Natarajan ShankarSRI International, USA
CPP-201810:30 - 11:00
Talk
Antal Spector-Zabusky, Joachim BreitnerUniversity of Pennsylvania, Christine RizkallahUniversity of Pennsylvania, USA, Stephanie WeirichUniversity of Pennsylvania, USA
DOI
CPP-201811:00 - 11:30
Talk
Damien RouhlingUniversity of Côte d'Azur, France
DOI
CPP-201811:30 - 12:00
Talk
Christian DoczkalCNRS, France, Joachim BardSaarland University, Germany
DOI