A Practical Decision Method for Propositional Dynamic Logic: Preliminary Report

We give a new characterization of the set of satisfiable formulae of propositional dynamic logic (PDL) based on the method of tableaux. From it we derive a heuristically efficient goal-directed proof procedure and a complete axiom system for PDL. The proof procedure illustrates a striking connection between natural deduction and symbolic execution. The completeness proof for the axiom system incorporates a method for the automatic synthesis of invariants. We also augment DL with new modalities throughout, during , and preserves , supply a new semantic foundation for DL programs, and show how to extend the satisfiability characterizations for PDL to throughout .

Authors

• Vaughan R. Pratt

Keywords

No keywords are indexed for this paper.