Checking Consistency of an ABox w.r.t. Global Assumptions in PDL

Issue title: Concurrency Specification and Programming (CS&P)

Article type: Research Article

Authors: Anh Nguyen, Linh | Szałas, Andrzej^;

Affiliations: Institute of Informatics, Warsaw University, Warsaw, Poland. nguyen@mimuw.edu.pl | Institute of Informatics, Warsaw University, Warsaw, Poland | Department of Computer and Information Science, Linköping University, Sweden. andsz@mimuw.edu.pl

Note: [] Address for correspondence: Institute of Informatics, Warsaw University, Banacha 2, 02-097 Warsaw, Poland

Abstract: We reformulate Pratt’s 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 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 a new result that the data complexity of the instance checking problem in PDL is coNP-complete.

DOI: 10.3233/FI-2010-299

Journal: Fundamenta Informaticae, vol. 102, no. 1, pp. 97-113, 2010