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

TL;DR

This paper introduces the first optimal, cut-free tableau decision procedure for the logic CPDLreg, combining Converse-PDL with regular inclusion axioms, enhancing efficiency through global caching and optimization techniques.

Contribution

It presents the first ExpTime tableau decision procedure for CPDLreg, extending Converse-PDL with regular inclusion axioms and incorporating optimization strategies.

Findings

The procedure is optimal and cut-free.

It employs global state caching for efficiency.

Includes on-the-fly propagation of consistency.

Abstract

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