Cicada implements a
reasoning architecture for checking ontology consistency for the description logic SHOIQ.
This architecture integrates algebraic reasoning
with tableaux for handling numerical restrictions imposed by
nominals and qualified cardinality restrictions.
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 a version of Cicada
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 SHOIQ ontologies that require other
optimization techniques. We built a set of synthetic test cases
to empirically evaluate our system. We compared Cicada with
major tableau-based 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,
inverse roles, and qualified cardinality restrictions than
traditional (hyper)tableau methods.
IBM ILOG CPLEX Optimization
Studio download
Cicada ZIP file
The SHOIQ ontology EU-Members.fowl.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 created EU-Members-inc.fowl.owl, which is inconsistent by trying to satisfy the existence of 29 EU members and the results show that Cicada is the only reasoner that classifies both variants in less that 10 seconds.
This small ontology CA-Provinces.fowl.owl defines 10 provinces of Canada using an enumeration of nominals. We created CA-Provinces_inc.fowl.owl, which is inconsistent by trying to satisfy the existence of 12 provinces of Canada and the results show that Cicada is the only reasoner that classifies both variants in less that 3 seconds.
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 40. The experiments show that only Cicada can process all these ontologies in less tan 20 seconds.
All OWL files as ZIP Archive