Support Page for "Pay-as-you-go Description Logic Reasoning by Coupling Tableau Algorithms with Completion-Based Saturation Procedures"

This page is in support of the paper "Pay-as-you-go Description Logic Reasoning by Coupling Tableau Algorithms with Completion-Based Saturation Procedures" (currently submitted to/under review at a journal), which presents a new coupling technique between tableau algorithms and completion-based saturation procedures to achieve pay-as-you-go reasoning for description logics. The technique is implemented in the reasoning system Konclude and significantly increases the performance for a wide range of ontologies. To make the results verifiable and reproducible, this page provides the links and downloads for the systems and datasets used in the evaluation.

Systems:

The evaluation of the coupling technique was conducted with the 64bit Linux version of Konclude v0.6.1, which is freely available under the terms of the LGPL 2.1 from Konclude's download page. The different saturation optimisations can separately be activated and deactivated with configurations files, which can be used by starting Konclude with the additional argument "-c config-file.xml" (see also Konclude's usage descriptions). Other reasoning systems that were used in the comparison can be downloaded from their homepages. In particular, FaCT++ v1.6.3 can be downloaded from https://code.google.com/p/factplusplus/, HermiT v1.3.8 from http://hermit-reasoner.com/, MORe v0.1.6 from https://code.google.com/p/more-reasoner/, and Pellet v2.3.1 from https://github.com/complexible/pellet/.

Datasets:

For the evaluation, we used all parsable and downloadable ontologies from the Gardiner ontology suite, the NCBO BioPortal, the NCIt archive, the OBO Foundry, the Oxford ontology library, the TONES repository, the subsets of the OWLCorpus that were gathered by the crawlers Google, OntoCrawler, OntoJCrawl, and Swoogle, and the ORE2014 dataset. In addition, we used several interesting benchmark ontologies for the evaluation.