Cardinality Restrictions Within Description Logic Connection Calculi

Recently, we have proposed the \( \theta \)-connection method for the description logic (DL) Open image in new window . It replaces the usage of Skolem terms and unification by additional annotation and introduces blocking through a new rule in the connection calculus, to ensure termination in the case of cyclic ontologies. In this work, we enhance this calculus and its representation to take on Open image in new window , an extended fragment that includes role hierarchies, qualified number restrictions and (in)equalities. The main novelty of the calculus lies in the introduction of equality, as well as in the redefinition of connection to accommodate number restrictions, either explicitly or expressed through equality. The new calculus uses the Eq system, thus introducing substitutivity axioms for each concept or role name. The application of Bibel’s equality connections appears here as a first solution to deal with equality.