From Tableaux to Automata for Description Logics

Issue title: The 1st International Workshop on Knowledge Representation and Approximate Reasoning (KR&AR)

Article type: Research Article

Authors: Baader, Franz | Hladik, Jan | Lutz, Carsten | Wolter, Frank

Affiliations: Theoretical Computer Science, TU Dresden, D-01062 Dresden, Germany | Department of Computer Science, University of Liverpool, Liverpool L69 7ZF, U.K.

Abstract: This paper investigates the relationship between automata-and tableau-based inference procedures for description logics. To be more precise, we develop an abstract notion of what a tableau-based algorithm is, and then 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.

Journal: Fundamenta Informaticae, vol. 57, no. 2-4, pp. 247-279, 2003