Expressive ABox Reasoning with Number Restrictions, Role Hierarchies, and Transitively Closed Roles
Volker Haarslev, Moeller Ralf · 2000
We present a new tableaux calculus deciding the ABox consistency problem for the expressive description logic ALCNH R + . Prominent language features of ALCNHR + are number restrictions, role hierarchies, transitively closed roles, and generalized concept inclusions. The ABox description logic system RACE is based on the calculus for ALCNH R + . 1 Introduction Experiences with concept languages indicate that at least description logics (DLs) with negation and disjunction are required to solve practical modeling problems without resorting to ad hoc extensions. The requirements derived from practical applications of DLs ask for even more expressive languages. For instance, in [14] the need for transitive roles is demonstrated for representing part-whole relations, family relations or partial orders in general. It is argued that the trade-o# between expressivity and complexity favors the integration of transitively closed roles instead of a transitive closure operator for roles. ...