View article

We present a simple ExpTime (complexity-optimal) tableau decision procedure based on and-or graphs with sound global caching for checking satisfiability of a concept w.r.t. a TBox in . Our algorithm is easy to implement and provides a foundation for ExpTime (complexity-optimal) tableau-based decision procedures for many modal and description logics, to which various optimisation techniques can be applied.