Nguyen, Linh Anh Szalas, Andrzej 2010 (English)In: Fundamenta Informaticae, ISSN 0169-2968, Vol. 102, no 1, 97-113Article in journal (Refereed) Published
We reformulate Pratts tableau decision procedure of checking satisfiability of a set of formulas in PDL. Our formulation is simpler and its implementation is more direct. Extending the method we give the first Ex PT m E (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 a new result that the data complexity of the instance checking problem in PDL is coNP-complete.
National CategoryEngineering and Technology
Identifiersurn:nbn:se:liu:diva-62154 (URN)10.3233/FI-2010-299 (DOI)000283643700008 (ISI)oai:DiVA.org:liu-62154 (OAI)diva2:371275 (DiVA)