Cicada implements a reasoning architecture for checking ontology consistency for the description logic SHOI. This architecture integrates algebraic reasoning with tableaux for handling numerical restrictions imposed by nominals. These numerical restrictions are mapped to linear inequality systems using a column generation and integer linear programming (ILP) formulation. The algebraic reasoner then processes these inequalities using a branch-and-price technique which is a combination of column generation and branch-and-bound technique. CPLEX has been used to solve our ILP formulation, which  is an optimization software tool for solving linear optimization problems.
We developed Cicada's first version (1.1.0) that implements our calculus as proof of concept. Besides the use of ILP and branch-and-price, this version only implements a few standard optimization techniques. Therefore, it might not perform well for SHOI ontologies that require other optimization techniques. We built a set of synthetic test cases to empirically evaluate our system. We compared Cicada with major OWL reasoners such as FaCT++ (version 1.6.5), HermiT (version 1.3.8) and Konclude (version 0.6.2). Our preliminary experiments indicate that Cicada performs better on ontologies having nominals and inverse roles than traditional (hyper)tableau methods.

IBM ILOG CPLEX Optimization Studio download
Cicada-1.1.0 ZIP file

Cicada Test Cases

OWL Files (in OWL functional syntax)

The ontology EU-Members.owl models 28 members of European Union (EU) by enumerating all 28 EU member states as nominals. All these 28 nominals are pairwise disjoint. We tested this ontology by trying to create 29 EU members and the results showed that only Cicada can identify that inconsistency within the time limit.
This is a small ontology CA-Provinces.owl that defines 10 provinces of Canada using an enumeration of nominals. 
This benchmark consists of small synthetic test ontologies that are using a variable n for representing the number of nominals. The first set consists of consistent and the second set of inconsistent ontologies. The variable n is increased from 5 to 20. The experiments show that only Cicada can process ontologies with more than 10 nominals within a reasonable amount of time.

All OWL files as ZIP Archive