Avalanche A Saturation-based Algebraic Reasoner
for the Description Logic SHQ

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.

More information about Avalanche:
A Saturation-based Algebraic Reasoner for ELQ
Jelena Vlasenko, Maryam Daryalal, Volker Haarslev, Brigitte Jaumard
Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning (PAAR 2016), Coimbra, Portugal, 2016, CEUR, pp. 110-124.
Acrobat file

Avalanche currently parses only SHQ ontologies expressed in RDF/XML syntax. Other formats might cause incorrect results.

IBM ILOG CPLEX Optimization Studio download
Avalanche ZIP file

Avalanche test files

OWL Files (in RDF/XML syntax)

All OWL files as ZIP archive