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.
Denition 1. The result of forgetting a set of symbols from an ontology O in a logic L is an ontology O such that sig(O ) = sig(O) n and for all L axioms with sig( ) \ = ; we have O j= i O j= .
Apart from TBox abduction and computing logical dierences between
ontology versions, forgetting has a lot of direct applications, and can be used to
hide condential information from an ontology, to analyse hidden relations
between concepts and roles, to generate ontology summaries, and has many more
applications, examples of which can found in [
Saturation-based reasoning has received increased interest in the last years by
the description logic community due to its good performance for classication.
Examples include the consequence-based reasoners used by ELK [
Common consequence-based reasoning methods do not enjoy these properties, since they are optimised towards classication. As example, take the following two axioms:
A1 v 8r:B
A2 v 8r::B Forgetting B from these axioms should result in the single axiom A1 uA2 v 8r:?. However, this inference is not necessary if we are only interested in entailments of the form A v B. Inferences between universal restrictions are usually not required for classication.
We developed a new family of saturation-based calculi for ALC, ALCH, SHQ
and SIF ontologies [
Furthermore, Lethe implements optimised variations of the forgetting
procedure to solve the related problems logical dierence and TBox abduction. The
aim of logical dierence is to compute diering entailments between ontology
versions with respect to some user-dened signature [
The form of abduction that is implemented in Lethe takes as input an
ontology O, a set of axioms Obs and a signature of abducibles , and computes
a logically weakest set of axioms H such that sig(H) and O [ H j= Obs.
TBox abduction can support ontology engineers in nding missing axioms of an
ontology if expected entailments are not satised. This problem can be reduced
to a form of forgetting by observing that O [ H j= Obs i O [ f:Obsg j= :H.
The negation of a TBox axiom C v D can be encoded in the TBox axiom
> v 9r :(Ci u :Di), where r is fresh. Using the technique described in [
Even though Lethe implements dierent calculi, these use similar techniques, which allows to implement a unied reasoning strategy. To give an idea, we Resolution Rule:
C1 t A
C2 t :A
C1 t C2 C t 9r:D
C
:D C1 t 8R:D1 C2 t QS:D2
C1 t C2 t QS:D12 where Q 2 f8; 9g and D12 is a possibly new dener representing
D1 u D2.
describe a simple calculus for ALC, introduced in [
The method requires the input to be normalised. Let Nc and Nr be the sets of concept symbols and role symbols that may be used in an ontology, and Nd Nc be a set of designated concept symbols called deners .
Denition 2. An ALC literal is a concept of the form A, :A, 9r:D, 8r:D, where D 2 Nd. An ALC literal of the form :D, D 2 Nd, is called negative dener literal . An ALC clause is an axiom of the form > v L1 t : : : t Ln, where every Li is an ALC literal. We usually omit the leading ‘ > v’ and assume that clauses are represented as sets, that is, they do not have duplicate literals and the order of the literals is not important. An ontology is in ALC normal form i every axiom is an ALC clause.
Every ALC ontology can be transformed into ALC normal form using
standard structural transformation and CNF transformation techniques. The
resulting ontology shares all entailments modulo deners with the original ontology.
If a normalised ALC ontology contains only clauses with at most one negative
dener literal, similar transformations can be applied in the other direction in
order to obtain an ontology without deners, which may use greatest xpoint
operators (see [
Example 1. For the ontology given in the introduction, a normalised representation is N = f:A1 t 8r:D1; :D1 t B; :A2 t 8r:D2; :D2 t :Bg.
The calculus ResALC is shown in Figure 1. A major dierence between our
calculi and calculi for consequence-based reasoning [
The calculi for ALCH ontologies, SHQ ontologies and ALC knowledge bases, as implemented in Lethe, use dierent rule sets, but the structure of these calculi is similar. They always have a resolution rule that allows to infer inferences on a specic symbol, and they have a set of combination rules, which lead to the introduction of new deners, and subsequently make further inferences possible.
In order to forget a concept symbol from the ontology, all inferences of the
resolution rule for which the conclusion contains maximally one negative dener
literal have to be performed. This may involve several applications of the
combination rules, as these lead to the introduction of new deners and clauses. In
the resulting clause set, all deners can be eliminated by applying the
normalisation backwards, resulting in an ontology without dener symbols, which may
use xpoint operators. As described in [
Central Reasoning Algorithm Used in Lethe The main challenge of implementing the calculi is to determine which applications of the combination rules are required in order to compute the forgetting result. If combination rules are applied unrestricted, we infer more clauses than necessary, and the implementation becomes impractical already for small ontologies. On the other hand, applications of the combination rules are necessary to make further inferences possible. Lethe uses an easy technique to ensure that all required inferences of combination rules are applied, while keeping the number of unnecessary inferences low. The idea is to use the resolution rule as guide to determine which deners should be introduced if possible. We can then determine how this dener can be introduced by using the combination rules.
Symbols to be forgotten are processed one after another, starting with the symbols with less occurrences in the ontology. For each symbol, we process only the portion of the ontology that uses this symbol. The main inference loop for forgetting a concept symbol A is then controlled by the following methods:
MAIN_LOOP. Process each negative occurrence of A one after another and perform all possible resolution steps. Pass the results to the method PROCESS_CLAUSE.
PROCESS_CLAUSE(C) . Determine whether the clause C contains more than one negative dener literal. If not, pass it to ADD_CLAUSE. Otherwise, we have C = :D1 t :D2 t C0. If there is a dener D12 that represents D1 t D2, replace C by :D12 t C0 and pass it again to PROCESS_CLAUSE. (This step basically performs resolution on the clauses :D12 t D1 and :D12 t D2, which are then also in the current clause set). If there is no such dener yet, look for occurrences of D1 and D2 under a role restriction and apply the corresponding role combination rules if possible, which may then introduce the dener D12. Every clause that is inferred in this process, as well as the clause :D12 t C0 if it could be generated, is sent again to PROCESS_CLAUSE, since it may again contain more than one negative dener symbol.
ADD_CLAUSE(C). We apply simplication rules on the clause and check whether it is redundant. If the clause does not contain the symbol to be eliminated, we add it to the nal output clause set.
Example 2. Assume we want to forget A from the clauses in the last example. MAIN_LOOP resolves on the clauses :D1 t A and :D2 t :A, and passes :D1 t :D2 to PROCESS_CLAUSE. As this clause contains more than one negative dener literal, we do not have to add it to the result. Instead, we check whether we can apply combination rules on clauses in which D1 and D2 occur under a role restriction. This is possible on the clauses :A1t8r:D1, :A2t8r:D2, and we pass the resulting clauses :A1 t:A2 t8r:D12, :D12 tD1, :D12 tD2 and :D12 to the method ADD_CLAUSE. The nal output contains only clauses with at most one negative dener literal, and no occurrences of B. The clause :D12 corresponds to the axiom D12 v ?. We can therefore replace D12 by ?. After some further syntactic adjustments we obtain the result A1 u A2 v 8r:?.
Several hash maps are used in the implementation to allow fast access of all occurrences of deners and the symbols that are currently forgotten. Throughout the computation, we ensure the invariant property that every stored clause contains maximally one negative dener literal. This is necessary to be able to eliminate introduced dener symbols in the end. 4
We evaluated the current version of Lethe on a set of 339 ontologies taken
from the NCBO BioPortal repository [
In around 9095% percent of cases, forgetting could be performed within 30 minutes. In most cases, the computation took just a few seconds, with the median of the duration being below 7 seconds in all cases. Except for the ALC forgetter with ABox support, the 90th percentile of the duration was always below 22 seconds.
Success Rate: 91.10% Without Fixpoints: 95.29% Duration Mean: 7.68 sec. Duration Median: 2.74 sec. Duration 90th percentile: 12.45 sec.
Success Rate: 94.79% Without Fixpoints: 92.91% Duration Mean: 23.94 sec. Duration Median: 3.01 sec. Duration 90th percentile: 29.00 sec.
Success Rate: 95.83% Without Fixpoints: 93.40% Duration Mean: 7.62 sec. Duration Median: 1.04 sec. Duration 90th percentile: 4.89 sec.
Success Rate: 88.10% Without Fixpoints: 93.27% Duration Mean: 18.03 sec. Duration Median: 3.81 sec. Duration 90th percentile: 21.17 sec.
Success Rate: 91.37% Fixpoints: 92.48% Duration Mean: 57.87 sec. Duration Median: 6.43 sec. Duration 90th percentile: 99.26 sec.
Success Rate: 90.77% Fixpoints: 91.99% Duration Mean: 13.51 sec.
Duration Median: 1.60 sec.
Duration 90th percentile: 11.65 sec. Lethe currently supports forgetting of concept and role symbols from ALCH ontologies and ALC knowledge bases with ABoxes, as well as forgetting concept symbols from SHQ ontologies. Apart from providing functionality for forgetting, Lethe uses these forgetting procedures together with dedicated optimisations for TBox abduction and computing logical dierences. The current version can be downloaded at http://www.cs.man.ac.uk/~koopmanp/lethe . It can be used as command line tool and as Java library. Furthermore, a simple GUI for computing and showing forgetting results on smaller ontologies is provided.
We currently have a prototypical implementation for SHI knowledge bases with ABoxes, which still has to be thoroughly tested and debugged. Even though our implementation of TBox abduction and logical dierences has been thoroughly optimised, a proper evaluation on realistic use cases is still open.
A natural next step is to develop and implement a method for SHIQ knowledge bases, which would generalise all three currently implemented methods. Though currently only used for forgetting, the calculi can in theory also be used for classical reasoning tasks such as satisability checking, classication or realisation. An interesting open question is how Lethe would perform as a reasoner if it is implemented towards these reasoning tasks. Another open question is whether our saturation-based reasoning approach can be used for other non-classical problems, such as for example approximation or ABox abduction.