Optimal and Cut-free Tableaux for Propositional Dynamic Logic with Converse

2010/02/01 by Goré, Rajeev, Widmann, Florian
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1002.0172

Abstract

We give an optimal (EXPTIME), sound and complete tableau-based algorithm for deciding satisfiability for propositional dynamic logic with converse (CPDL) which does not require the use of analytic cut. Our main contribution is a sound methodto combine our previous optimal method for tracking least fix-points in PDL with our previous optimal method for handling converse in the description logic ALCI. The extension is non-trivial as the two methods cannot be combined naively. We give sufficient details to enable an implementation by others. Our OCaml implementation seems to be the first theorem prover for CPDL.

Related

• A Cut-Free ExpTime Tableau Decision Procedure for the Logic Extending\n Converse-PDL with Regular Inclusion Axioms
• An On-the-fly Tableau-based Decision Procedure for PDL-Satisfiability
• Tableaux for Dynamic Logic of Propositional Assignments
• ExpTime Tableaux for Type PDL
• Cut-Free ExpTime Tableaux for Checking Satisfiability of a Knowledge\n Base in the Description Logic SHI