LETHE: A Saturation-Based Tool for Non-Classical Reasoning

Koopmann, P. and Schmidt, R. A. (2015)

In Dumontier, et al (eds), Proceedings of the 4th International Workshop on OWL Reasoner Evaluation (ORE-2015). CEUR Workshop Proceedings, Vol. 1387, CEUR-WS.org, BiBTeX, PDF.

We present the saturation-based reasoning system LETHE. LETHE is a tool that can be used for uniform interpolation, forgetting, TBox abduction and logical difference. To solve these problems, LETHE uses saturation-based reasoning to eliminate certain symbols from an ontology, such that entailments in the remaining vocabulary are preserved. This is known as forgetting or uniform interpolation. LETHE is an implementation of our forgetting methods for various expressive description logics, and can be used as a Java library and as a standalone tool for the mentioned reasoning tasks. We give a high level description of the calculi used by LETHE, describe the reasoning algorithm implemented in LETHE, and give an evaluation of the system on realistic ontologies.


Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 21 Oct 15
Copyright © 2015 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk