# ExpTime Tableaux with Global Caching for Hybrid PDL

## 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.

## Key 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.

---
Source: https://tomesphere.com/paper/1705.00848