# An Overview of Tableau Algorithms for Description Logics

Studia Logica - An International Journal for Symbolic Logic, no. 1 (2001): 5-40

EI

Description logics are a family of knowledge representation formalisms that are descended from semantic networks and frames via the system Kl-one. During the last decade, it has been shown that the important reasoning problems (like subsumption and satisfiability) in a great variety of description logics can be decided using tableau-like ...更多

0

• Description logics (DLs) are a family of knowledge representation languages which can be used to represent the terminological knowledge of an application domain in a structured and formally well-understood way.
• An ABox is a finite set of assertions of the form C(a) or r(a, b), where C is a concept description, r a role name, and a, b are individual names.
• Given the input description Cn, the satisfiability algorithm generates a complete and open ABox whose canonical interpretation is a binary tree of depth n, and consists of 2n+1 − 1 individuals.

• Description logics (DLs) are a family of knowledge representation languages which can be used to represent the terminological knowledge of an application domain in a structured and formally well-understood way
• The name description logics is motivated by the fact that, on the one hand, the important notions of the domain are described by concept descriptions, i.e., expressions that are built from atomic concepts and atomic roles using the concept and role constructors provided by the particular DL
• Though many of the tableau-based algorithms sketched in this paper are of optimal worst-case complexity, and provide complexity results for subsumption and satisfiability in DLs, theoretical complexity results never were the main focus of this line of DL research
• For the logics treated in Section 6.2, the exact worst-case complexity (EXPTIME) was known before the (NEXPTIME) tableau algorithms sketched above were designed
• When the first complexity results showed that all of the DLs used in systems had subsumption problems of a higher complexity, the proposed solution was either to restrict the expressive power or to employ incomplete algorithms

• For ALCQ, the idea that leads to a PSPACE-algorithm for ALCN with non-unary notation does no longer work: it is not sufficient to introduce just one successor as representative for the role successors required by at-least restrictions.
• Satisfiability of ALCQ-concept descriptions as well as consistency of ALCQ-ABoxes are PSPACE-complete problems, even if numbers are not represented in unary notation.
• Nebel (1990b) shows that this complexity can, in general, not be avoided: for the DL FL0, which allows for conjunction and value restriction only, subsumption between concept descriptions can be tested in polynomial time, whereas subsumption w.r.t. acyclic terminologies is coNP-complete.
• In order to obtain a PSPACE-algorithm for subsumption in ALC w.r.t. acyclic terminologies, one cannot first apply unfolding to the concept descriptions to be tested for subsumption since this may need exponential space.
• . Internalisation of this axiom introduces a new transitive role u, and asserts in the role hierarchy that u is a super-role of all roles occurring in C and the concept description C0 to be tested for satisfiability.
• It shows that satisfiability and subsumption of concept descriptions in SH is EXPTIME-hard.5 The tableau algorithm for SH presented in (Horrocks, 1998b) handles role hierarchies by an appropriate definition of r-successors: an individual y is called an r-successor of an individual x in an ABox A iff s(x, y) ∈ A for some sub-role s of r.
• This violates the value restriction for x1, which shows that the interpretation obtained this way is not a model of the complete and open ABox. This problem can be overcome by using equality blocking, i.e., an individual y is blocked by an individual x iff {D | D(x) ∈ A} = {D | D (y) ∈ A}.

• If the role hierarchy contains the axiom s r for a transitive role r ∈ NR+, the following concept is obviously satisfiable, but each of its models has an infinite s-path: ¬A ∃s.A ∀r.(∃s.A ( 1s−)).
• This problem can be overcome by applying the pre-completion technique, which reduces ABox consistency to satisfiability of concept descriptions.
• It turned out that implementations of these algorithms were amenable to optimisation techniques and behaved quite well in practice (Baader et al, 1994; Bresciani et al, 1995)

• Description logics (DLs) are a family of knowledge representation languages which can be used to represent the terminological knowledge of an application domain in a structured and formally well-understood way.
• An ABox is a finite set of assertions of the form C(a) or r(a, b), where C is a concept description, r a role name, and a, b are individual names.
• Given the input description Cn, the satisfiability algorithm generates a complete and open ABox whose canonical interpretation is a binary tree of depth n, and consists of 2n+1 − 1 individuals.
• For ALCQ, the idea that leads to a PSPACE-algorithm for ALCN with non-unary notation does no longer work: it is not sufficient to introduce just one successor as representative for the role successors required by at-least restrictions.
• Satisfiability of ALCQ-concept descriptions as well as consistency of ALCQ-ABoxes are PSPACE-complete problems, even if numbers are not represented in unary notation.
• Nebel (1990b) shows that this complexity can, in general, not be avoided: for the DL FL0, which allows for conjunction and value restriction only, subsumption between concept descriptions can be tested in polynomial time, whereas subsumption w.r.t. acyclic terminologies is coNP-complete.
• In order to obtain a PSPACE-algorithm for subsumption in ALC w.r.t. acyclic terminologies, one cannot first apply unfolding to the concept descriptions to be tested for subsumption since this may need exponential space.
• . Internalisation of this axiom introduces a new transitive role u, and asserts in the role hierarchy that u is a super-role of all roles occurring in C and the concept description C0 to be tested for satisfiability.
• It shows that satisfiability and subsumption of concept descriptions in SH is EXPTIME-hard.5 The tableau algorithm for SH presented in (Horrocks, 1998b) handles role hierarchies by an appropriate definition of r-successors: an individual y is called an r-successor of an individual x in an ABox A iff s(x, y) ∈ A for some sub-role s of r.
• This violates the value restriction for x1, which shows that the interpretation obtained this way is not a model of the complete and open ABox. This problem can be overcome by using equality blocking, i.e., an individual y is blocked by an individual x iff {D | D(x) ∈ A} = {D | D (y) ∈ A}.
• If the role hierarchy contains the axiom s r for a transitive role r ∈ NR+, the following concept is obviously satisfiable, but each of its models has an infinite s-path: ¬A ∃s.A ∀r.(∃s.A ( 1s−)).
• This problem can be overcome by applying the pre-completion technique, which reduces ABox consistency to satisfiability of concept descriptions.
• It turned out that implementations of these algorithms were amenable to optimisation techniques and behaved quite well in practice (Baader et al, 1994; Bresciani et al, 1995)

• Table1: Syntax and semantics of concept descriptions. From the modal logic point of view, roles are simply names for accessibility relations, and existential (value) restrictions correspond to diamonds (boxes) indexed by the respective accessibility relation. Thus, any ALC description can be translated into a multi-modal K formula and vice versa. For example, the description P ∃r.P ∀r.¬P corresponds to the formula p ∧ r p ∧ [r]¬p, where p is an atomic proposition corresponding to the concept name P . As pointed out by <a class="ref-link" id="cSchild_1991_a" href="#rSchild_1991_a">Schild (1991</a>), there is an obvious correspondence between the semantics of ALC and the Kripke semantics for
• Table2: Syntax and semantics of role constructors and restrictions   