ExpTime Tableaux with Global Caching for Hybrid PDL
Linh Anh Nguyen
TL;DR
This paper introduces the first direct tableau decision procedure with ExpTime complexity for HPDL, combining global caching and fulfillment checks, suitable for practical reasoning in description logics.
Contribution
It presents a novel ExpTime tableau decision procedure for HPDL that integrates global caching with handling of nominals and eventualities, with implementation details included.
Findings
Decides satisfiability of HPDL ABoxes efficiently
Achieves ExpTime complexity for the decision procedure
Implemented in the TGC2 system for practical use
Abstract
We present the first direct tableau decision procedure with the ExpTime complexity for HPDL (Hybrid Propositional Dynamic Logic). It checks whether a given ABox (a finite set of assertions) in HPDL is satisfiable. Technically, it combines global caching with checking fulfillment of eventualities and dealing with nominals. Our procedure contains enough details for direct implementation and has been implemented for the TGC2 (Tableaux with Global Caching) system. As HPDL can be used as a description logic for representing and reasoning about terminological knowledge, our procedure is useful for practical applications.
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.