A Cut-Free ExpTime Tableau Decision Procedure for the Logic Extending\n Converse-PDL with Regular Inclusion Axioms

2011/04/03 by Linh Anh Nguyen, Nguyen, Linh Anh
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Natural Language Processing Techniques #semigroups and automata theory

paper · pdf · doi:10.48550/arxiv.1104.0405

openalex publication_date 2011/04/03 · openalex created_date 2022/10/04 · openalex updated_date 2026/07/28

Abstract

We give the first cut-free ExpTime (optimal) tableau decision procedure for\nthe logic CPDLreg, which extends Converse-PDL with regular inclusion axioms\ncharacterized by finite automata. The logic CPDLreg is the combination of\nConverse-PDL and regular grammar logic with converse. Our tableau decision\nprocedure uses global state caching and has been designed to increase\nefficiency and allow various optimization techniques, including on-the-fly\npropagation of local and global (in)consistency.\n

Citations

• A near-optimal method for reasoning about action

Related

• Optimal and Cut-free Tableaux for Propositional Dynamic Logic with\n Converse
• ExpTime Tableaux with Global Caching for Hybrid PDL
• Cut-Free ExpTime Tableaux for Checking Satisfiability of a Knowledge\n Base in the Description Logic SHI
• An On-the-fly Tableau-based Decision Procedure for PDL-Satisfiability
• ExpTime Tableaux for Type PDL