Skip to main navigation Skip to search Skip to main content

Lethe: Saturation-based reasoning for non-standard reasoning tasks

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

Abstract

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.
Original languageEnglish
Title of host publicationInformal Proceedings of the 4th International Workshop on OWL Reasoner Evaluation, ORE-2015 - co-located with the 28th International Workshop on Description Logics, DL 2015
EditorsM. Horridge, G. Stamou, G. Stoilos, M. Dumontier, B. Parsia, N. Matentzoglu, R. Goncalves, B. Glimm, E. Jimenez-Ruiz
PublisherCEUR Workshop Proceedings
Pages23-30
Publication statusPublished - 2015
Externally publishedYes
Event4th International Workshop on OWL Reasoner Evaluation, ORE-2015 - co-located with the 28th International Workshop on Description Logics, DL 2015 - Athens, Greece
Duration: 6 Jun 2015 → …

Publication series

NameCEUR Workshop Proceedings
ISSN (Print)1613-0073

Conference

Conference4th International Workshop on OWL Reasoner Evaluation, ORE-2015 - co-located with the 28th International Workshop on Description Logics, DL 2015
Country/TerritoryGreece
CityAthens
Period6/06/15 → …

Fingerprint

Dive into the research topics of 'Lethe: Saturation-based reasoning for non-standard reasoning tasks'. Together they form a unique fingerprint.

Cite this