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
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