This talk investigates the relationship between automata- and tableau-based inference procedures for Description Logics. After a short introduction into Description Logics, it will sketch and compare the known automata- and tableau-based inference procedures. Then, it will introduce an abstract notion of what a tableau-based algorithm is, and show, on this abstract level, how tableau-based algorithms can be converted into automata-based algorithms. In particular, this allows us to characterize a large class of tableau-based algorithms that imply an ExpTime upper-bound for reasoning in the Description Logics for which such an algorithm exists.
(This is joint work with Jan Hladik, Carsten Lutz, and Frank Wolter.)