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.

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.
  • Koala-5.owl
  • Koala-10.owl
  • Koala-15.owl
  • Koala-20.owl
  
  
• 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.
• European-Union-28.owl
• European-Union-30.owl


• Paper Ontology O₁
• Paper-10.owl
• Paper-15.owl
  

All OWL files as ZIP archive