Checking Consistency of an ABox w.r.t. Global Assumptions in PDL
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: urn:nbn:se:liu:diva-62154DOI: 10.3233/FI-2010-299ISI: 000283643700008OAI: oai:DiVA.org:liu-62154DiVA: diva2:371275