Cut-Free ExpTime Tableaux for Converse-PDL Extended with Regular Inclusion Axioms
Nguyen Linh Anh · Frontiers in artificial intelligence and applications · 2013
We develop a cut-free tableau calculus for the logic CPDLreg, leading to the first cut-free EXPTIME (optimal) tableau decision procedure for CPDLreg. This logic extends Converse-PDL with regular inclusion axioms characterized by finite automata. It is a logical formalism suitable for expressing complex properties of agents' cooperation in terms of beliefs, goals and intentions.