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 semantic 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 respectively two Ackermann-based forgetting methods developed in our recent work. Both can be used as standalone tools or Java libraries for forgetting 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.
Ontologies, exploiting Description Logics as the representational underpinning,
provide a logic-based data model for representation of domain knowledge thereby
supporting e ective 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
nonstandard 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 speci c 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 [
Forgetting can be de ned in two closely related ways; it can be de ned
syntactically as the dual of uniform interpolation [
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
implementations 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 [
ALCOI H(O; u) and ALCOQH(O; :; u; t) Let NC, NR and NI be three countably in nite and pairwise disjoint sets of concept names, role names and individual names (nominals ), respectively. Roles in ALCOIH(O; u) can be a role name r 2 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: > j ? j a j A j :C j C u D j C t D j 9R:C j 8R:C, where a 2 NI, A 2 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 2 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: > j ? j a j A j :C j C u D j C t D j mR:C j nR:C, where a 2 NI, A 2 NC, C and D are arbitrary concepts, R is an arbitrary role, and m 1 and n 0 are natural numbers. Further concepts are de ned as abbreviations: 9R:C = 1R:C, 8R: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 (quali ed) 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 nite set of axioms of the form C v D (concept inclusions ), where C and D are any concepts. An RBox is a nite set of axioms of the form r v s (role inclusions ), where r; s 2 NR. An ABox is a nite set of axioms of the form C(a) (concept assertions ) and r(a; b) (role assertions ), where a; b 2 NI, r 2 NR, and C is any concept. ABox assertions are super uous 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 9r: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 de ned 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, 9R:C or 8R: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 nite 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 2 NC (S 2 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 concept 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 2 NC (S 2 NR) be any concept (role) name, and let I and I0 be any interpretations. We say that I and I0 are equivalent up to S, or S-equivalent, if I and I0 coincide but di er possibly in the interpretation of S. More generally, we say that I and I0 are equivalent up to a set F of concept and role names, or F -equivalent, if I and I0 coincide but di er possibly in the interpretations of the names in F .
De nition 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 i the following conditions hold: (i) sig(O0) sig(O)nF , and (ii) for any interpretation I: I j= O0 i I0 j= O, for some interpretation I0 F -equivalent to I, i.e., O and O0 are equivalent up to the interpretations of the names in F .
De nition 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)nF i the following conditions hold: (i) sig(O0) sig(O)nF , and (ii) for any axiom with sig( ) sig(O)nF , O0 j= i O j= , i.e., O0 preserves all logical consequences over the names in sig(O)nF .
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
Fame 1.0 and 2.0 eliminate concept and role names in a goal-oriented manner. In this section, we brie y 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 2 sigC(N ) from a set N of clauses when A is pure in N . Speci cally, 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 puri cation. The Ackermann rules, shown in Figure 1, are applied to eliminate a concept name A 2 sigC(N ) from a set N of clauses when A is impure in N . By N nfC1 t A; :::; Cn t Ag 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.
N nfC1 t A; :::; Cn t Ag; C1 t A; :::; Cn t A
N nfC1 t A; :::; Cn t Ag:AC1t:::t:Cn provided: (i) A 2 sigC(N ) is the pivot, (ii) the Ci (1 i
n) do not contain A, and (iii) A occurs only negatively in N nfC1 t A; :::; Cn t Ag. AckermannC; provided: (i) A 2 sigC(N ) is the pivot,
N nfC1 t :A; :::; Cn t :Ag; C1 t :A; :::; Cn t :A
N nfC1 t :A; :::; Cn t :AgCA1u:::uCn (ii) A does not occur in the Ci (1 i
n), and (iii) A occurs only positively in N nfC1 t :A; :::; Cn t :Ag. De nition 3 (A-Reduced Form for ALCOIH(O; u)). For A 2 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 2 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 i for some interpretation I0 A-equivalent to I, the premises are true in I0, 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 di erent from the calculus described above for concept name elimination, 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 de ner introduction rules.
PT+(r)
PR+(r) 3. Ground-tier: fCi t 9(t1 u : : : u tw u Qi):Dig 3. 1st-tier: [ fCi t Ej t 9(t1 u : : : u tw u Qi):(Di u Fj )g
fCi t Ej1 t Ej2 t 9(t1 u : : : u tw u Qi):(Di u Fj1 u Fj2 )g 3. 2nd-tier: 3. . . .
1 j n
[ 1 j1 j2 n 3. nth-tier: fCi t E1 t : : : t En t 9(t1 u : : : u tw u Qi):(Di u F1 u : : : u Fn)g. 2. Block(P (r); :sk t r) denotes the following set: 3. fE1 t 8sk:F1; : : : ; En t 8sk:Fn; :sk t t1; : : : ; :sk t twg.
( ( ? Ej = ? if PT = ;
Fj = > if PT = ;
(
O if PR = ; tl otherwise.
The purify rules eliminate a role name r 2 sigR(N ) from a set N of clauses when r is pure in N . Speci cally, 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 i N is in r-reduced form.
De nition 4 (r-Reduced Form for ALCOIH(O; u)). For r 2 NR the pivot, a TBox clause is in r-reduced form if it has the form C t 9(r u Q):D or C t 8r: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 t r 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 de ner 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 re exive, i.e., r v r . Theorem 3. Let I be any ALCOIH(O; u)-interpretation. For r 2 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 i for some interpretation I0 r-equivalent to I, the premises are true in I0, i.e., the conclusion of the rule is a semantic solution of forgetting r from N .
Theorem 4. The rewrite rules preserve equivalence. The de ner introduction rules preserve equivalence up to the interpretation of the introduced de ners.
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 di erences in the speci cations 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
Owl/Xml file
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 speci ed as an Owl/Xml le, or as a URL pointing to an Owl/Xml le, though, internally, Fame uses own data structure for e ciency. 3 http://owlcs.github.io/owlapi/ Algorithm 1: forget(r sig, c sig, clause set)
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 return clause set end initialising nal int sig size before to (r sig.size() + c sig.size()) initialising SethNamei pure sig to null /* get from r sig and c sig all names that are pure in clause set pure sig := getPureNames(r sig, c sig, clause set) /* apply Purify to clause set to eliminate names in pure sig clause set := purify(pure sig, clause set) /* simplify all axioms in clause set clause set.getSimpli ed() initialising SethClausei sub clause set to null foreach RoleName role in r sig do /* get from clause set all axioms that contain role sub clause set := getSubset(role, clause set) /* remove from clause set all axioms in sub clause set clause set.removeAll(sub clause set); /* attempt to transform sub clause set into r-reduced form sub clause set.getRReducedForm(role, sub clause set); /* check whether sub clause set is in r-reduced form if isRReducedForm(role, role clause set) then /* apply AckermannR to sub clause set to eliminate role sub clause set := ackermann(role, sub clause set) /* simplify all axioms in sub clause set sub clause set.getSimpli ed() /* add the resulting set sub clause set back to clause set clause set.addAll(sub clause set) /* remove role from r sig r sig.remove(role) /* add all introduced definer names to c sig c sig.addAll(sub clause set.getDe ners()) else 22 23 end 24 Similar for loop over the concept names in the present c sig 25 initialising nal 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 /* add the unchanged set sub clause set back to clause set clause set.addAll(sub clause set) */ */ */ */ */ */ */ */ */ */ */ */ */ */ */
Fame defaults to performing role forgetting rst. This is because during the role forgetting process concept de ner names may be introduced (to facilitate the normalisation of the input ontology). These de ner 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 = fr1; :::; rm; A1; :::; Ang, where ri 2 sigR(O) (1 i m) and Aj 2 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 (clausi cation), (ii) the role forgetting phase, (iii) the concept forgetting phase, and (iv) the conversion of the resulting set N 0 of clauses into an ontology O0 (declausi cation). 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 puri cation 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 simpli ed, leading to a much reduced set with fewer clauses and fewer names. This makes subsequent forgetting less di cult. 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 simpli cations are then performed on the resulting subset (i.e., the elimination and the simplication are performed locally ). This signi cantly reduces the search space and has improved the e ciency of Fame (compared to the early prototypes). It is found that a name that could not be eliminated by Fame might become eliminable 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 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 [
The expressivity of the ontologies in the snapshot ranges from E L 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 reformulations as summarised in Table 1, which also lists the types of axioms that TBox ABox
#(O) #sigC(O) #sigR(O) #sigI(O)
Type of Axiom
SubClassOf(C1 C2) EquivalentClasses(C1 C2)
DisjointClasses(C1 C2)
DisjointUnion(C C1. . . Cn)
SubObjectPropertyOf(R1 R2) EquivalentObjectProperties(R1 R2)
ObjectPropertyDomain(R C) ObjectPropertyRange(R C)
ClassAssertion(C a) ObjectPropertyAssertion(R a1 a2)
Representation
SubClassOf(C1 C2) SubClassOf(C1 C2), SubClassOf(C2 C1)
SubClassOf(C1 ObjectComplementOf(C2)) EquivalentClasses(C ObjectUnionOf(C1. . . Cn))
DisjointClasses(C1. . . Cn) SubObjectPropertyOf(R1 R2) SubObjectPropertyOf(R1 R2)
SubObjectPropertyOf(R2 R1) SubClassOf(ObjectSomeValuesFrom(R owl:Thing), C)
SubClassOf(owl:Thing ObjectAllValuesFrom(R C))
SubClassOf(a C)
SubClassOf(a1 ObjectSomeValuesFrom(R a2)) 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 information 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 re ect real-world application scenarios, we evaluated the performance of Fame 1.0 and 2.0 for eliminating di erent 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 ndings. A timeout of 1000 seconds was used on each run.
The results obtained from eliminating di erent 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 respectively 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., eliminated all speci ed concept and role names and the possibly introduced de ners, 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 solutions were computed within four seconds (the current versions include several signi cant 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 De ner shows the percentages of cases where the introduced de ners 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 [
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
Press, 2017. 26. Y. Zhao and R. A. Schmidt. On Concept Forgetting in Description Logics with
Press, 2018.