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 dierence. 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.
Lethe is a tool that can be used for uniform interpolation, forgetting,
TBox abduction and logical dierence. 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 language | Undefined |
|---|---|
| Title of host publication | CEUR Workshop Proceedings |
| Pages | 23-30 |
| Number of pages | 8 |
| Volume | 1387 |
| Publication status | Published - 6 Jun 2015 |
Keywords
- Biomineralization
- Birds
- Formal language
- Interpolation