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:
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.
EuropeanUnionconcept, 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 the EU concept is unsatisfiable, in this case, all the other reasoners timed out and could not determine the unsatisfiability.
All OWL files as ZIP archive