An Optimal Tableau Decision Procedure for Converse-PDL
Linh Anh Nguyen, Andrzej Szałas · 2009
We give a novel tableau calculus and an optimal (EXPTIME) tableau decision procedure based on the calculus for the satisfiability problem of propositional dynamic logic with converse. Our decision procedure is formulated with global caching and can be implemented together with useful optimization techniques.