=Paper=
{{Paper
|id=Vol-2211/paper-37
|storemode=property
|title=The FAME Family: A Family of Reasoning Tools for Forgetting in Expressive Description
Logics
|pdfUrl=https://ceur-ws.org/Vol-2211/paper-37.pdf
|volume=Vol-2211
|authors=Yizheng Zhao,Hao Feng,Ruba Alassaf,Warren Del-Pinto,Renate A. Schmidt
|dblpUrl=https://dblp.org/rec/conf/dlog/ZhaoFADS18
}}
==The FAME Family: A Family of Reasoning Tools for Forgetting in Expressive Description
Logics==
https://ceur-ws.org/Vol-2211/paper-37.pdf
The FAME Family – A Family of Reasoning
Tools for Forgetting in Expressive Description
Logics
Yizheng Zhao1 , Hao Feng2 , Ruba Alassaf1 , Warren Del-Pinto1 and
Renate A. Schmidt1
1
The University of Manchester, UK
2
North China University of Science and Technology, China
Abstract. We present the Fame family – a family of reasoning tools for
forgetting in expressive description logics. Forgetting is a non-standard
reasoning service that seeks to create restricted views of (description
logic-based) ontologies by eliminating a set of concept and role names,
namely the forgetting signature, from the ontologies in such a way that
all logical consequences are preserved up to the remaining signature. The
family has two members at present: (i) Fame 1.0 for computing seman-
tic solutions of forgetting in the description logic ALCOIH(O, u), and
(ii) Fame 2.0 for computing uniform interpolants in the description logic
ALCOQH(O, ¬, u, t). They are Java-based implementations of respec-
tively two Ackermann-based forgetting methods developed in our recent
work. Both can be used as standalone tools or Java libraries for forget-
ting and related tasks. An empirical evaluation of Fame 1.0 and 2.0 on
a large corpus of real-world ontologies shows that the tools are practical.
1 Introduction
Ontologies, exploiting Description Logics as the representational underpinning,
provide a logic-based data model for representation of domain knowledge thereby
supporting effective reasoning over domain knowledge for a range of real-world
applications, most evidently for applications in life sciences, text mining, as well
as the Semantic Web. However, with their growing utilisation, not only has the
number of available ontologies increased considerably, but they are often large
in size and are becoming more complex to manage. Moreover, modelling domain
knowledge in the form of ontologies is labour-intensive work which is expensive
from an implementation perspective. There is therefore a strong demand for
technologies and automated tools for creating restricted views of ontologies so
that existing ontologies can be reused to their full potential. Forgetting is a non-
standard reasoning service that seeks to create restricted views of ontologies by
eliminating a set of concept and role names, namely the forgetting signature,
from the ontologies in such a way that all logical consequences are preserved up
to the remaining signature. It allows users to focus on specific parts of ontologies
that can be easily reused, or to zoom in on ontologies for in-depth analysis of
certain subparts. Other uses of forgetting can be found in [9,16,7,13,20,18,4,3].
Forgetting can be defined in two closely related ways; it can be defined syntac-
tically as the dual of uniform interpolation [19] (related notions include weak for-
getting [21], consequence-based inseparability [15] and consequence-based con-
servative extensions [6]) and it can be defined model-theoretically as semantic
forgetting [20] (related notions include strong forgetting [12], model insepara-
bility [8], model conservative extensions [14] and second-order quantifier elimi-
nation [5]). The two notions differ in the sense that uniform interpolation pre-
serves all logical consequences up to certain names whereas semantic forgetting
preserves equivalence up to certain names. In this sense, semantic forgetting is
a stronger notion of forgetting than uniform interpolation, and the results of
semantic forgetting, namely the semantic solutions, are in general stronger than
those of uniform interpolation, namely the uniform interpolants. Semantic solu-
tions often require more expressivity than is available in the source language. For
example, the semantic solution of forgetting the role name {r} from the ALC-
ontology {A1 v ∃r.B, A2 v ∀r.¬B} is {A1 v ∃O.B, A1 u A2 v ⊥}, whereas the
uniform interpolant is {A1 u A2 v ⊥}, which is weaker. Observe that the target
language must include the universal role O to represent the semantic solution. If
a semantic solution is expressible in the source logic, then it is equivalent to the
uniform interpolant, which means, in this case, the two notions coincide [21].
In this paper, we describe the Fame family – a family of reasoning tools for
forgetting in expressive description logics. The Fame family has two members
at present, namely, Fame 1.0 and Fame 2.0, which are Java-based implementa-
tions of respectively the methods of [23,24] for computing semantic solutions of
forgetting in the description logic ALCOIH(O, u), and the methods of [25,26] for
computing uniform interpolants in the description logic ALCOQH(O, ¬, u, t).
The foundations for the methods are non-trivial generalisations of Ackermann’s
Lemma [1]. The universal role and the Boolean role constructors enrich the tar-
get languages, rendering them more expressive to represent forgetting solutions.
Fame 1.0 is the first tool for computing semantic solutions of forgetting in de-
scription logics. Fame 2.0 is the first tool for computing uniform interpolants in
description logics with qualified number restrictions plus nominals and ABoxes.
Both tools have been evaluated on a large corpus of real-world ontologies, with
the results showing that: (i) in more than 90% of the test cases the tools were
successful, i.e., eliminated all specified concept and role names and the possibly
introduced definers, and (ii) in more than 70% of the successful cases the elimi-
nation was done within seconds. The current versions of Fame 1.0 and 2.0 can
be downloaded via http://www.cs.man.ac.uk/~schmidt/sf-fame/.
2 ALCOIH(O, u) and ALCOQH(O, ¬, u, t)
Let NC , NR and NI be three countably infinite and pairwise disjoint sets of con-
cept names, role names and individual names (nominals), respectively. Roles in
ALCOIH(O, u) can be a role name r ∈ NR , the inverse r− of a role name r, the
universal role O, or can be formed with conjunction. Concepts in ALCOIH(O, u)
have one of the following forms: > | ⊥ | a | A | ¬C | C uD | C tD | ∃R.C | ∀R.C,
where a ∈ NI , A ∈ NC , C and D are arbitrary concepts, and R is an arbitrary
role. Roles in ALCOQH(O, ¬, u, t) can be a role name r ∈ NR , the universal
role O, or can be formed with negation, conjunction and disjunction. Concepts
in ALCOQH(O, ¬, u, t) have one of the following forms: > | ⊥ | a | A | ¬C | C u
D | C t D | ≥mR.C | ≤nR.C, where a ∈ NI , A ∈ NC , C and D are arbitrary
concepts, R is an arbitrary role, and m ≥ 1 and n ≥ 0 are natural numbers. Fur-
ther concepts are defined as abbreviations: ∃R.C = ≥1R.C, ∀R.C = ≤0R.¬C,
¬≥mR.C = ≤nR.C and ¬≤nR.C = ≥mR.C, where n = m − 1. Concepts of the
form ≥mR.C and ≤nR.C are called (qualified) number restrictions, which allow
one to specify cardinality constraints on roles.
An ALCOIH(O, u)- or ALCOQH(O, ¬, u, t)-ontology comprises of a TBox,
an RBox and an ABox. A TBox is a finite set of axioms of the form C v D
(concept inclusions), where C and D are any concepts. An RBox is a finite set
of axioms of the form r v s (role inclusions), where r, s ∈ NR . An ABox is a finite
set of axioms of the form C(a) (concept assertions) and r(a, b) (role assertions),
where a, b ∈ NI , r ∈ NR , and C is any concept. ABox assertions are superfluous
in description logics with nominals, because they can be expressed equivalently
as concept inclusions (via nominals), namely, C(a) as a v C and r(a, b) as a v
∃r.b. Hence, an ALCOIH(O, u)- or ALCOQH(O, ¬, u, t)-ontology is assumed
to contain only TBox and RBox axioms. The semantics of ALCOIH(O, u) and
ALCOQH(O, ¬, u, t) is defined as usual.
The forgetting methods used by Fame 1.0 and 2.0 work on TBox and RBox
axioms in clausal normal form. A TBox literal in ALCOIH(O, u) is a concept of
the form a, ¬a, A, ¬A, ∃R.C or ∀R.C. A TBox literal in ALCOQH(O, ¬, u, t)
is a concept of the form a, ¬a, A, ¬A, ≥mR.C or ≤nR.C. A TBox clause is a
disjunction of a finite number of TBox literals. An RBox atom in ALCOIH(O, u)
is a role name, an inverted role name or the universal role. An RBox atom in
ALCOQH(O, ¬, u, t) is a role name or the universal role. An RBox clause is a
disjunction of an RBox atom and a negated RBox atom. TBox and RBox clauses
are obtained from corresponding axioms using the standard clausal normal form
transformations.
Let S ∈ NC (S ∈ NR ) be a designated concept (role) name. We say that an
occurrence of S is positive (negative) in an axiom or clause if it is under an even
(odd ) number of negations. An axiom (clause) is called an S-axiom (S-clause) if
it contains S. An axiom (clause) is called an S + -axiom (S + -clause) or S − -axiom
(S − -clause) if it contains positive (negative) occurrences of S. S is said to be
pure in a set N of clauses if either all occurrences of S in N are positive, or all
occurrences of S in N are negative. It is said to be impure otherwise.
By sigC (X), sigR (X) and sigI (X), we denote respectively the sets of the con-
cept names, role names and individual names occurring in X, where X ranges
over concepts, roles, clauses, axioms, sets of clauses and ontologies. By sig(X) we
denote the union of sigC (X) and sigR (X). Let S ∈ NC (S ∈ NR ) be any concept
(role) name, and let I and I 0 be any interpretations. We say that I and I 0 are
equivalent up to S, or S-equivalent, if I and I 0 coincide but differ possibly in the
interpretation of S. More generally, we say that I and I 0 are equivalent up to a
set F of concept and role names, or F-equivalent, if I and I 0 coincide but differ
possibly in the interpretations of the names in F.
Definition 1 (Semantic Forgetting). Let O be an ontology and let F ⊆
sig(O) be the forgetting signature. An ontology O0 is a semantic solution of
forgetting F from O iff the following conditions hold: (i) sig(O0 ) ⊆ sig(O)\F,
and (ii) for any interpretation I: I |= O0 iff I 0 |= O, for some interpretation I 0
F-equivalent to I, i.e., O and O0 are equivalent up to the interpretations of the
names in F.
Definition 2 (Uniform Interpolation). Let O be an ontology and let F ⊆
sig(O) be the forgetting signature. An ontology O0 is a uniform interpolant of O
for sig(O)\F iff the following conditions hold: (i) sig(O0 ) ⊆ sig(O)\F, and (ii)
for any axiom α with sig(α) ⊆ sig(O)\F, O0 |= α iff O |= α, i.e., O0 preserves
all logical consequences over the names in sig(O)\F.
In this paper, the notation F is used to denote the forgetting signature, i.e.,
the set of concept and role names to be forgotten, and FC and FR are used to
denote respectively the sets of the concept names and the role names in F. The
name in F under current consideration for forgetting is referred to as the pivot.
3 The Calculi
Fame 1.0 and 2.0 eliminate concept and role names in a goal-oriented manner.
In this section, we briefly go through the calculi used respectively by Fame 1.0
and 2.0 for eliminating a concept and a role name from an ALCOIH(O, u)- and
an ALCOQH(O, ¬, u, t)-ontology (in clausal form). For proofs and other details
of the calculi, we refer to reader to the original work [23,24,25,26].
3.1 Eliminating One Concept Name in ALCOIH(O, u)
The calculus used by Fame 1.0 for eliminating a concept name from a set of
ALCOIH(O, u)-clauses includes three types of rules: (i) two purify rules, (ii)
two Ackermann rules, and (iii) four rewrite rules.
The purify rules are applied to eliminate a concept name A ∈ sigC (N ) from
a set N of clauses when A is pure in N . Specifically, A is eliminated from N by
substituting > (⊥) for every occurrence of A in N if all occurrences of A in N
are positive (negative). This is referred to as purification. The Ackermann rules,
shown in Figure 1, are applied to eliminate a concept name A ∈ sigC (N ) from a
set N of clauses when A is impure in N . By N \{C1 t A, ..., Cn t A} we denote
the set N excluding the clauses C1 t A, ..., Cn t A. By NαA we denote the clause
set obtained from N by substituting α for every occurrence of A in N , where α
is a concept. While the purify rules can be applied at any time, the Ackermann
rules can only be applied if N is in A-reduced form.
AckermannC,+
N \{C1 t A, ..., Cn t A}, C1 t A, ..., Cn t A
N \{C1 t A, ..., Cn t A}A¬C1 t...t¬Cn
provided: (i) A ∈ sigC (N ) is the pivot,
(ii) the Ci (1 ≤ i ≤ n) do not contain A, and
(iii) A occurs only negatively in N \{C1 t A, ..., Cn t A}.
AckermannC,−
N \{C1 t ¬A, ..., Cn t ¬A}, C1 t ¬A, ..., Cn t ¬A
N \{C1 t ¬A, ..., Cn t ¬A}A C1 u...uCn
provided: (i) A ∈ sigC (N ) is the pivot,
(ii) A does not occur in the Ci (1 ≤ i ≤ n), and
(iii) A occurs only positively in N \{C1 t ¬A, ..., Cn t ¬A}.
Fig. 1: Ackermann rules for eliminating A ∈ sigC (N ) from a set N of clauses
Definition 3 (A-Reduced Form for ALCOIH(O, u)). For A ∈ NC the pivot,
a clause is in A+ -reduced form if it has the form C t A, and is in A− -reduced
form if it has the form C t ¬A, where C is a clause that does not contain A. A
set N of clauses is in A-reduced form if all A+ -clauses in N are in A+ -reduced
form, or all A− -clauses in N are in A− -reduced form.
The rewrite rules attempt to transform an A-clause (not in A-reduced form)
into an equivalent one in A-reduced form. Note that using the present calculus,
a concept name cannot always be eliminated. This is because there is a gap in
the scope of the rewrite rules, which means that transforming a clause set into
A-reduced form is not always possible.
Theorem 1. Let I be an ALCOIH(O, u)-interpretation. For A ∈ NC the pivot,
when an Ackermann/a purify rule is applicable to a set N of ALCOIH(O, u)-
clauses, the conclusion of the rule is true in I iff for some interpretation I 0
A-equivalent to I, the premises are true in I 0 , i.e., the conclusion of the rule is
a semantic solution of forgetting A from N .
Theorem 2. The rewrite rules preserve equivalence.
3.2 Eliminating One Role Name in ALCOIH(O, u)
Slightly different from the calculus described above for concept name elimina-
tion, the calculus used by Fame 1.0 for eliminating a role name from a set of
ALCOIH(O, u)-clauses includes four types of rules: (i) two purify rules, (ii) one
Ackermann rule, (iii) three rewrite rules, and (iv) four definer introduction rules.
AckermannR
T
P + (r) P + (r)
z }| { z R
}| {
N , C1 t ∃(r u Q1 ).D1 , . . . , Cm t ∃(r u Qm ).Dm , ¬s1 t r, . . . , ¬sv t r,
T
P − (r) P − (r)
R
z }| { z }| {
E1 t ∀r.F1 , . . . , En t ∀r.Fn , ¬r t t1 , . . . , ¬r t tw
N , Block(P − (r), C1 t ∃(r u Q1 ).D1 ), ..., Block(P − (r), Cm t ∃(r u Qm ).Dm ),
Block(P − (r), ¬s1 t r), ..., Block(P − (r), ¬sv t r)
provided: (i) r ∈ NR is the pivot,
(ii) r does not occur in N , and
(iii) the premises are in r-reduced form.
Notation in the AckermannR rule (1 ≤ i ≤ m, 1 ≤ j ≤ n, 1 ≤ k ≤ v, 1 ≤ l ≤ w):
1. Block(P − (r), Ci t ∃(r u Qi ).Di ) denotes the union of the following sets:
3. Ground-tier: {Ci t ∃(t1 u . . . u tw u Qi ).Di }
[
3. 1st-tier: {Ci t Ej t ∃(t1 u . . . u tw u Qi ).(Di u Fj )}
1≤j≤n
[
3. 2nd-tier: {Ci t Ej1 t Ej2 t ∃(t1 u . . . u tw u Qi ).(Di u Fj1 u Fj2 )}
1≤j1 ≤j2 ≤n
3. . . .
3. nth-tier: {Ci t E1 t . . . t En t ∃(t1 u . . . u tw u Qi ).(Di u F1 u . . . u Fn )}.
2. Block(P − (r), ¬sk t r) denotes the following set:
3. {E1 t ∀sk .F1 , . . . , En t ∀sk .Fn , ¬sk t t1 , . . . , ¬sk t tw }.
( ( (
⊥ if PT− = ∅ > if PT− = ∅ O −
if PR =∅
? Ej = Fj = tl =
Ej otherwise, Fj otherwise, and tl otherwise.
Fig. 2: Ackermann rule for eliminating r ∈ sigR (N ) from a set N of clauses
The purify rules eliminate a role name r ∈ sigR (N ) from a set N of clauses
when r is pure in N . Specifically, r is eliminated from N by substituting the
universal role (the empty role) for every occurrence of r in N if all occurrences of
r in N are positive (negative). When r is impure in N , we apply the Ackermann
rule, shown in Figure 2, to N to eliminate r. The Ackermann rule is applicable
to N to eliminate r iff N is in r-reduced form.
Definition 4 (r-Reduced Form for ALCOIH(O, u)). For r ∈ NR the pivot,
a TBox clause is in r-reduced form if it has the form C t ∃(r u Q).D or C t ∀r.D,
where C (D) is a clause (concept) that does not contain r, and Q is a role that
does not contain r. An RBox clause is in r-reduced form if it has the form ¬S tr
or ¬r t S, where S 6= r is a role name, or S 6= r− is an inverted role name. A
set N of clauses is in r-reduced form if all r-clauses in N are in r-reduced form.
The rewrite rules and the definer introduction rules [22] attempt to transform
an r-clause (not in r-reduced form) into r-reduced form. The transformation is
not always possible; it fails in cases where r is reflexive, i.e., r v r− .
Theorem 3. Let I be any ALCOIH(O, u)-interpretation. For r ∈ NR the pivot,
when the Ackermann/a purify rule is applicable to a set N of ALCOIH(O, u)-
clauses, the conclusion of the rule is true in I iff for some interpretation I 0
r-equivalent to I, the premises are true in I 0 , i.e., the conclusion of the rule is
a semantic solution of forgetting r from N .
Theorem 4. The rewrite rules preserve equivalence. The definer introduction
rules preserve equivalence up to the interpretation of the introduced definers.
The calculi used by Fame 2.0 for eliminating a concept (role) name from a
set of ALCOQH(O, ¬, u, t)-clauses are analogous to the present calculus used by
Fame 1.0 for role name elimination, with slight differences in the specifications
of reduced forms and generalisations of Ackermann rules. For space reasons, we
do not describe them in this paper. For those who are interested in the details
of the calculi used by Fame 2.0, we refer to [25,26].
4 The Implementation
Load ontology Parse into own Role forgetting
data structure
Parse into
Save ontology Owl/Xml file Concept forgetting
Fig. 3: Top-level design of Fame 1.0 and 2.0
Fame 1.0 and 2.0 were implemented in Java and have the same architecture,
as shown in Figure 3. Hence in this section, we use the name “Fame” to refer to
both versions. Fame uses the OWL API Version 3.5.63 for the tasks of loading,
parsing and saving ontologies. The ontology to be loaded must be specified as an
Owl/Xml file, or as a URL pointing to an Owl/Xml file, though, internally,
Fame uses own data structure for efficiency.
3
http://owlcs.github.io/owlapi/
Algorithm 1: forget(r sig, c sig, clause set)
Input : a set r sig of role names to be forgotten
a set c sig of concept names to be forgotten
a set clause set of clauses
Output: a set clause set of clauses (after forgetting)
1 do
2 if r sig is empty and c sig is empty then
/* clause set does not contain any names in r sig or c sig; in
this case, clause set is a forgetting solution */
3 return clause set
4 end
5 initialising final int sig size before to (r sig.size() + c sig.size())
6 initialising SethNamei pure sig to null
/* get from r sig and c sig all names that are pure in clause set */
7 pure sig := getPureNames(r sig, c sig, clause set)
/* apply Purify to clause set to eliminate names in pure sig */
8 clause set := purify(pure sig, clause set)
/* simplify all axioms in clause set */
9 clause set.getSimplified()
10 initialising SethClausei sub clause set to null
11 foreach RoleName role in r sig do
/* get from clause set all axioms that contain role */
12 sub clause set := getSubset(role, clause set)
/* remove from clause set all axioms in sub clause set */
13 clause set.removeAll(sub clause set);
/* attempt to transform sub clause set into r-reduced form */
14 sub clause set.getRReducedForm(role, sub clause set);
/* check whether sub clause set is in r-reduced form */
15 if isRReducedForm(role, role clause set) then
/* apply AckermannR to sub clause set to eliminate role */
16 sub clause set := ackermann(role, sub clause set)
/* simplify all axioms in sub clause set */
17 sub clause set.getSimplified()
/* add the resulting set sub clause set back to clause set */
18 clause set.addAll(sub clause set)
/* remove role from r sig */
19 r sig.remove(role)
/* add all introduced definer names to c sig */
20 c sig.addAll(sub clause set.getDefiners())
21 else
/* add the unchanged set sub clause set back to clause set */
22 clause set.addAll(sub clause set)
23 end
24 Similar for loop over the concept names in the present c sig
25 initialising final int sig size after to (r sig.size() + c sig.size())
26 while sig size before != sig size after
/* clause set still contains names in r sig or c sig */
27 return clause set
Fame defaults to performing role forgetting first. This is because during the
role forgetting process concept definer names may be introduced (to facilitate the
normalisation of the input ontology). These definer names, regarded as regular
concept names, can thus be eliminated as part of subsequent concept forgetting.
Given an ontology O and a forgetting signature F = {r1 , ..., rm , A1 , ..., An },
where ri ∈ sigR (O) (1 ≤ i ≤ m) and Aj ∈ sigC (O) (1 ≤ j ≤ n), the forgetting
process in Fame consists of four phases: (i) the conversion of O into a set N of
clauses (clausification), (ii) the role forgetting phase, (iii) the concept forgetting
phase, and (iv) the conversion of the resulting set N 0 of clauses into an ontol-
ogy O0 (declausification). The concept (role) forgetting phase is an iteration of
several rounds in which the concept (role) names in F are eliminated using the
corresponding calculus described in the previous section and the work of [25,26].
The main algorithm used by Fame is shown in Algorithm 1. Fame performs
purification prior to other steps (Lines 6–9). This is because the purify rules do
not require the clause set to be normalised or to be transformed into a reduced
form, and they can be applied at any time. Moreover, applying the purify rules
to a clause set often results in numerous syntactic redundancies, tautologies and
contradictions inside the clauses which are immediately eliminated or simplified,
leading to a much reduced set with fewer clauses and fewer names. This makes
subsequent forgetting less difficult. The getSubset(S, O) method extracts from
the clause set O all axioms that contain the name S. S can thus be eliminated
from this subset, rather than from the entire set O. Subsequent simplifications
are then performed on the resulting subset (i.e., the elimination and the simpli-
fication are performed locally). This significantly reduces the search space and
has improved the efficiency of Fame (compared to the early prototypes). It is
found that a name that could not be eliminated by Fame might become elim-
inable after the elimination of another name [24]. We therefore impose a do-while
loop on the iterations of the elimination rounds. The breaking condition checks
if there were names eliminated during the previous elimination rounds. If so,
Fame repeats the iterations, attempting to eliminate the remaining names. The
loop terminates when the forgetting signature becomes empty or no names were
eliminated during the previous elimination rounds.
5 The Evaluation
The current versions of Fame 1.0 and 2.0 were evaluated on a large corpus of
ontologies taken from the NCBO BioPortal repository, a resource that currently
includes more than 600 ontologies originally developed for clinical research. The
corpus for evaluation was based on a snapshot of the repository taken in March
2017 [17], containing 396 OWL API compatible ontologies.
The expressivity of the ontologies in the snapshot ranges from EL and ALC to
SHOIN and SROIQ. Since Fame 1.0 (2.0) can handle ontologies as expressive
as ALCOIH(O, u) (ALCOQH(O, ¬, u, t)), we adjusted these ontologies to the
language of ALCOIH(O, u) (ALCOQH(O, ¬, u, t)). This involved simple refor-
mulations as summarised in Table 1, which also lists the types of axioms that
Type of Axiom Representation
SubClassOf(C1 C2) SubClassOf(C1 C2)
EquivalentClasses(C1 C2) SubClassOf(C1 C2), SubClassOf(C2 C1)
DisjointClasses(C1 C2) SubClassOf(C1 ObjectComplementOf(C2))
EquivalentClasses(C ObjectUnionOf(C1. . . Cn))
DisjointUnion(C C1. . . Cn)
DisjointClasses(C1. . . Cn)
TBox
SubObjectPropertyOf(R1 R2) SubObjectPropertyOf(R1 R2)
SubObjectPropertyOf(R1 R2)
EquivalentObjectProperties(R1 R2)
SubObjectPropertyOf(R2 R1)
ObjectPropertyDomain(R C) SubClassOf(ObjectSomeValuesFrom(R owl:Thing), C)
ObjectPropertyRange(R C) SubClassOf(owl:Thing ObjectAllValuesFrom(R C))
ClassAssertion(C a) SubClassOf(a C)
ABox
ObjectPropertyAssertion(R a1 a2) SubClassOf(a1 ObjectSomeValuesFrom(R a2))
Table 1: Types of axioms that can be handled by Fame
Maximum Minimum Mean Median 90th percentile
#(O) 1833761 100 4651 1096 12570
#sigC (O) 847760 36 2110 502 5598
#sigR (O) 1390 0 54 12 144
#sigI (O) 87879 0 216 0 206
Table 2: Statistics of the ontologies used for evaluation
can be handled by Fame 1.0 (2.0). Concepts not expressible in ALCOIH(O, u)
(ALCOQH(O, ¬, u, t)) were replaced by >. Table 2 shows statistical informa-
tion about the adjusted ontologies, where #(O) denotes the number of axioms
in the ontologies, and #sigC (O), #sigR (O) and #sigI (O) denote respectively the
numbers of concept names, role names and individual names in the ontologies.
To reflect real-world application scenarios, we evaluated the performance of
Fame 1.0 and 2.0 for eliminating different numbers of concept and role names
from each ontology. In particular, we considered the cases of eliminating 10%,
40% and 70% of concept and role names in the signature of each ontology. The
names to be forgotten were randomly chosen. The experiments were run on a
desktop computer with an Intelr Coretm i7-4790 processor, four cores running
at up to 3.60 GHz and 8 GB of DDR3-1600 MHz RAM. The experiments were
run 100 times on each ontology and we averaged the results in order to verify
the accuracy of our findings. A timeout of 1000 seconds was used on each run.
The results obtained from eliminating different numbers of concept and role
names from the ALCOIH(O, u)-ontologies (computed by Fame 1.0) and from
the ALCOQH(O, ¬, u, t)-ontologies (computed by Fame 2.0) are shown respec-
tively in Table 3 and Table 4. The most encouraging results are that: on average,
(i) Fame 1.0 (2.0) was successful in more than 90% of the test cases, i.e., elimi-
nated all specified concept and role names and the possibly introduced definers,
and (ii) in most of the ALCOIH(O, u)-cases forgetting solutions were computed
within one second, and in most of the ALCOQH(O, ¬, u, t)-cases forgetting so-
Settings Results
#FC (avg) Time (sec) Timeouts Success Rate Nominal Clause Growth
211 (10%) 0.307 1.8% 94.9% 7.6% -10.3%
844 (40%) 0.895 3.4% 93.4% 17.4% -41.2%
1477 (70%) 1.364 6.6% 90.2% 24.7% -72.4%
#FR (avg) Time (sec) Timeouts Success Rate Definer Clause Growth
5 (10%) 0.309 0.0% 100.0% 0.0% 0.9%
22 (40%) 0.977 2.5% 97.5% 0.0% 3.5%
38 (70%) 1.891 6.6% 93.4% 0.0% 6.7%
Table 3: Evaluation results of Fame 1.0
Settings Results
#FC (avg) Time (sec) Timeouts Success Rate Definer Semantic
214 (10%) 1.265 1.0% 96.5% 2.5% 25.0%
856 (40%) 3.901 3.8% 90.4% 5.8% 8.8%
1498 (70%) 7.272 7.6% 82.3% 10.1% 5.3%
#FR (avg) Time (sec) Timeouts Success Rate Definer Clause Growth
6 (10%) 0.778 0.0% 100.0% 0.0% 3.5%
26 (40%) 2.654 3.5% 96.5% 0.0% 14.8%
45 (70%) 4.906 9.1% 90.9% 0.0% 23.7%
Table 4: Evaluation results of Fame 2.0
lutions were computed within four seconds (the current versions include several
significant improvements over the prototypes used in [23,24,25,26]).
Because of one rewrite rule in the calculus for concept name elimination in
ALCOIH(O, u) [24], fresh nominals might be introduced during the forgetting
process, but these nominals cannot be eliminated from the forgetting solutions
using the methods of Fame 1.0. The column headed Nominal in Table 3 suggests
however that forgetting solutions containing fresh nominals only occurred in a
small number of cases (≤ 25%). The column headed Definer shows the percent-
ages of cases where the introduced definers could not be all eliminated from the
forgetting solutions. Observe that, in concept forgetting, there was a decrease in
the number of clauses in the forgetting solutions (compared to the input clause
set), but in role forgetting, there was on the contrary an increase; see the Clause
Growth column. As elaborated previously, the uniform interpolant computed by
Fame 2.0 in concept forgetting could also be a semantic solution. The column
headed Semantic shows that on average, in 13.2% of the test cases, the uniform
interpolant was also a semantic solution. This means that semantic solutions of
concept forgetting are rare for ALCOQH(O, ¬, u, t).
The most closely related tools to the Fame family are Lethe [10,11] and the
tool developed by [13]. Both use resolution-based methods for computing uniform
interpolants for ALC TBoxes, and in the case of Lethe several extensions of
ALC TBoxes. An empirical comparison of Fame 1.0 and 2.0 with Lethe has
shown that Fame 1.0 and 2.0 are considerably faster than Lethe [2].
References
1. W. Ackermann. Untersuchungen über das Eliminationsproblem der mathematis-
chen Logik. Mathematische Annalen, 110(1):390–413, 1935.
2. R. Alassaf and R. A. Schmidt. A Preliminary Comparison of the Forgetting So-
lutions Computed using SCAN, LETHE and FAME. In Proc. SOQE’17, volume
2013 of CEUR Workshop Proceedings, pages 21–26. CEUR-WS.org, 2017.
3. E. Botoeva, B. Konev, C. Lutz, V. Ryzhikov, F. Wolter, and M. Zakharyaschev.
Inseparability and Conservative Extensions of Description Logic Ontologies: A Sur-
vey. In Proc. RW’16, volume 9885 of LNCS, pages 27–89. Springer, 2016.
4. W. Del-Pinto and R. A. Schmidt. Forgetting-Based Abduction in ALC. In Proc.
SOQE’17, volume 2013 of CEUR Workshop Proceedings, pages 27–35. CEUR-
WS.org, 2017.
5. D. M. Gabbay, R. A. Schmidt, and A. Szalas. Second Order Quantifier Elimination:
Foundations, Computational Aspects and Applications. College Publications, 2008.
6. S. Ghilardi, C. Lutz, and F. Wolter. Did I Damage My Ontology? A Case for
Conservative Extensions in Description Logics. In Proc. KR’06, pages 187–197.
AAAI Press, 2006.
7. B. C. Grau and B. Motik. Reasoning over Ontologies with Hidden Content: The
Import-by-Query Approach. J. Artif. Intell. Res., 45:197–255, 2012.
8. B. Konev, C. Lutz, D. Walther, and F. Wolter. Model-theoretic inseparability and
modularity of description logic ontologies. Artif. Intell., 203:66–103, 2013.
9. B. Konev, D. Walther, and F. Wolter. Forgetting and Uniform Interpolation in
Large-Scale Description Logic Terminologies. In Proc. IJCAI’09, pages 830–835.
IJCAI/AAAI Press, 2009.
10. P. Koopmann. Practical Uniform Interpolation for Expressive Description Logics.
PhD thesis, University of Manchester, UK, 2015.
11. P. Koopmann and R. A. Schmidt. LETHE: saturation-based reasoning for non-
standard reasoning tasks. In Proc. DL’15, volume 1387 of CEUR Workshop Pro-
ceedings, pages 23–30. CEUR-WS.org, 2015.
12. F. Lin and R. Reiter. Forget it! In Proc. AAAI Fall Symposium on Relevance,
pages 154–159. AAAI Press, 1994.
13. M. Ludwig and B. Konev. Practical Uniform Interpolation and Forgetting for ALC
TBoxes with Applications to Logical Difference. In Proc. KR’14. AAAI Press, 2014.
14. C. Lutz, D. Walther, and F. Wolter. Conservative Extensions in Expressive De-
scription Logics. In Proc. IJCAI’07, pages 453–458. AAAI/IJCAI Press, 2007.
15. C. Lutz and F. Wolter. Deciding inseparability and conservative extensions in the
description logic EL. J. Symb. Comput., 45(2):194–228, 2010.
16. C. Lutz and F. Wolter. Foundations for Uniform Interpolation and Forgetting in
Expressive Description Logics. In Proc. IJCAI’11, pages 989–995. IJCAI/AAAI
Press, 2011.
17. N. Matentzoglu and B. Parsia. BioPortal Snapshot 30.03.2017, Mar. 2017.
18. N. Nikitina and S. Rudolph. (Non-)Succinctness of uniform interpolants of general
terminologies in the description logic EL. Artif. Intell., 215:120–140, 2014.
19. A. Visser. Bisimulations, Model Descriptions and Propositional Quantifiers. Logic
Group Preprint Series. Department of Philosophy, Utrecht University, 1996.
20. K. Wang, Z. Wang, R. W. Topor, J. Z. Pan, and G. Antoniou. Eliminating Con-
cepts and Roles from Ontologies in Expressive Descriptive Logics. Computational
Intelligence, 30(2):205–232, 2014.
21. Y. Zhang and Y. Zhou. Forgetting Revisited. In Proc. KR’10. AAAI Press, 2010.
22. Y. Zhao. Automated Semantic Forgetting for Expressive Description Logics. PhD
thesis, The University of Manchester, UK, 2017.
23. Y. Zhao and R. A. Schmidt. Concept Forgetting in ALCOI-Ontologies Using An
Ackermann Approach. In Proc. ISWC’15, volume 9366 of LNCS, pages 587–602.
Springer, 2015.
24. Y. Zhao and R. A. Schmidt. Forgetting Concept and Role Symbols in
ALCOIHµ+ (O, u)-Ontologies. In Proc. IJCAI’16, pages 1345–1352. IJCAI/AAAI
Press, 2016.
25. Y. Zhao and R. A. Schmidt. Role Forgetting for ALCOQH(O)-Ontologies Using An
Ackermann-Based Approach. In Proc. IJCAI’17, pages 1354–1361. IJCAI/AAAI
Press, 2017.
26. Y. Zhao and R. A. Schmidt. On Concept Forgetting in Description Logics with
Qualified Number Restrictions. In Proc. IJCAI’18, pages 1984–1990. IJCAI/AAAI
Press, 2018.