Checking Consistency of an ABox w.r.t. Global Assumptions in PDL
Linköping University, Department of Computer and Information Science, KPLAB - Knowledge Processing Lab
Linköping University, The Institute of Technology
Article in journal (Refereed)
Fundamenta Informaticae(ISSN 0169-2968)
Engineering and Technology
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.