Unification in a Description Logic with Inconsistency and Transitive Closure of Roles
F. Baader and R. Küsters
Unification of concept descriptions was introduced by Baader and Narendran as a new inference service for detecting and avoiding redundancies in description logic (DL) knowledge bases. Unification considers concept patterns, i.e., concept descriptions with variables, and tries to make these descriptions equivalent by replacing the variables by appropriate concept descriptions. Baader and Narendran have shown that unification in FL0, a DL that allows for the top concept, concept conjunction, and value restrictions, unification is an ExpTime-complete problem. This result was extended by Baader and Kuesters, who have shown that unification is still ExpTime-complete for the DL FLreg, which extends FL0 by the role constructors union, composition, and transitive closure. They also showed that solvable FLreg-unification problem always have least unifiers. In the present paper we extend these results to a DL, which extends FLreg by the bottom concept. This result strongly depends on the existence of least unifiers in FLreg.