Avalanche implements a reasoning architecture for deciding
subsumption for the description logic SHQ, which is a subset of
the Web Ontology Language (OWL). Avalanche combines saturation
rules with algebraic reasoning based on Integer Linear Programming
(ILP). Deciding numerical satisfiability of a set of qualified
cardinality restrictions is reduced to constructing a
corresponding system of linear inequalities and applying ILP
methods in order to determine whether this system is feasible. The
ILP component is based on IBM ILOG CPLEX Optimization Studio (see
link below) that is freely available for academic research. Our
preliminary experiments indicate that this calculus offers a
better scalability for qualified cardinality restrictions than
approaches combining both tableaux and ILP as well as traditional
(hyper)tableau methods.
Avalanche currently parses only SHQ ontologies expressed in
RDF/XML syntax. Other formats might cause incorrect results.
All OWL files as ZIP archive