Optimal Tableau Decision Procedures for PDL
Logic in Computer Science
2011-04-12 v2 Artificial Intelligence
Computational Complexity
Abstract
We reformulate Pratt's tableau decision procedure of checking satisfiability of a set of formulas in PDL. Our formulation is simpler and more direct for implementation. Extending the method we give the first EXPTIME (optimal) tableau decision procedure not based on transformation for checking consistency of an ABox w.r.t. a TBox in PDL (here, PDL is treated as a description logic). We also prove the new result that the data complexity of the instance checking problem in PDL is coNP-complete.
Cite
@article{arxiv.0904.0721,
title = {Optimal Tableau Decision Procedures for PDL},
author = {Linh Anh Nguyen and Andrzej Szałas},
journal= {arXiv preprint arXiv:0904.0721},
year = {2011}
}