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.

More information about the foundation of CARON:
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

IBM ILOG CPLEX Optimization Studio download

CARON Test Cases

OWL Files (in OWL functional syntax)

All OWL files as ZIP archive