Tags:alchq formula, connection method, description logic, equality and qualified number restrictions
Abstract:
Abstract. Recently, we have proposed the θ-connection method for the description logic (DL) ALC, the ALC θ-CM. It replaces the usage of Skolem terms and unification by additional annotation and introduces blocking, a typical feature of DL provers, by a new rule, to ensure termination in the case of cyclic ontologies. In this work, we enhance this calculus and its representation to take on ALCHQ++, the extended fragment that includes role Hierarchies, Qualified number restrictions and (in)equalities. The calculus' main enhancement lies in the introduction of (in)equalities, as well as the redefinition of connection so as to accommodate number restrictions, either explicitly or expressed though equalities. The application of Bibel’s eq-connections (equality connections) consists in a first solution to deal with (in)equalities. Termination, soundness and completeness of the calculus are proven, complementing the proofs presented for the ALC θ-CM.
Cardinality Restrictions within Description Logic Connection Calculi