Optimal Tableau Decision Procedures for PDL
Linh Anh Nguyen, Andrzej Sza{\l}as
TL;DR
This paper introduces a simplified tableau decision procedure for PDL, achieving optimal EXPTIME complexity and establishing coNP-completeness of data complexity for instance checking, advancing description logic reasoning methods.
Contribution
It presents the first EXPTIME tableau decision procedure for PDL that does not rely on transformations, and proves coNP-completeness of data complexity in PDL.
Findings
Simplified tableau procedure for PDL satisfiability
First EXPTIME tableau decision method without transformation
Data complexity of instance checking is coNP-complete
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Semantic Web and Ontologies · Advanced Database Systems and Queries