We present an algorithm for solving the unification problem in the description logic FL_bottom. This logic extends FL_0 with the bottom constructor and thus supports conjunction, value restrictions, top and bottom. Unification of concepts may become a useful tool for ontology maintenance; however, little is known about unification even in small, restricted description logics. The unification problem has been solved only for FL_0 and EL. This paper contributes to the ongoing effort to extend these results to richer logics. Our algorithm runs in exponential time with respect to the size of the problem.

Unification in Description Logics has been introduced as a means to detect redundancies in ontologies. We try to extend the known decidability results for unification in the Description Logic EL to disunification since negative constraints on unifiers can be used to avoid unwanted unifiers. While decidability of the solvability of general EL-disunification problems remains an open problem, we obtain NP-completeness results for two interesting special cases: dismatching problems, where one side of each negative constraint must be ground, and local solvability of disunification problems, where we restrict the attention to solutions that are built from so-called atoms occurring in the input problem. More precisely, we first show that dismatching can be reduced to local disunification, and then provide two complementary NP-algorithms for finding local solutions of (general) disunification problems.

We give a set of inference rules with constant constraints. Then we show how to extend a set of equational clauses, so that if the application of these inference rules halts on these clauses, then the theory is decidable by applying a standard set of Paramodulation inference rules. In addition, we can determine the number of clauses generated in this decision procedure. For some theories, such as the theory of lists, there are 0(n /spl times/ lg(n)) clauses. For others it is polynomial. And for others it is simply exponential such as the theory of (extensional) arrays.