# A Consequence-based Algebraic Reasoner for the Description Logic SHOQ

CARON (Consequence-based Algebraic Reasoning about nOminals and Number restrictions) currently implements classification of OWL ontologies specified in the ALCOQ subset of SHOQ. Other standard description logic services such as concept satisfiability and Abox reasoning are also supported, through rewriting them as Tbox axioms using nominals. In this first version of our prototype, we focused more on implementing a sound and complete system that terminates in a reasonable amount of time. The underlying algorithm handles the arithmetic interaction between qualified cardinality restrictions (number restrictions) and nominals using atomic decomposition and integer linear programming. Our preliminary performance evaluation is very promising and shows the practicability of our approach. CARON relies on IBM ILOG CPLEX Optimization Studio for implementing integer linear programming.

A Consequence-based Algebraic Calculus for SHOQ
Nikoo Zolfaghar Karahroodi, Volker Haarslev
Proceedings of the 30th International Workshop on Description Logics (DL 2017), Montpellier, France, July, 2017.
Acrobat file

CARON ZIP file

### CARON Test Cases

#### OWL Files (in OWL functional syntax)

• Koala Ontology
The first test case is the Koala ontology which is a simple ontology about marsupials and humans. It is based on description logic ALCON, and is part of the Protégé ontology library. Since CARON does not support datatypes, we have ignored axioms containing them. We extended this ontology by a new concept `MaleStudentwith(n)Daughters`, where we increase n from 5 to 20. Although, CARON does not have the best run time, but it is consistent with the other state-of-the-art description logic reasoners.
• European Union Ontology
The second test case European Union is designed based on the Countries ontology, which represents the ISO 3166 Code list of countries. Accordingly, we have defined `EuropeanUnion` concept, which represents the European Union (EU) with exactly n members that are located in Europe and all members are instances of `EUMemberState`, which represents European Union member states as enumeration of 28 nominals. When $n > 28$ the EU concept is unsatisfiable, in this case, all the other reasoners timed out and could not determine the unsatisfiability.

• Paper Ontology O1

All OWL files as ZIP archive