This paper is concerned with the problem of computing the semantic di erence between di erent versions of large-scale ontologies using a uniform interpolation (UI) approach. The semantic di erence between two versions of an ontology are the axioms entailed by one version but not the other, re ecting the semantic evolutionary changes of the ontology. We develop a novel, tailor-made UI method for the task of computing semantic di erence in large-scale ontologies, which often speci ed in the description logic ELH. The method is terminating and sound, and can always compute results of UI when such results exist. A case study on di erent versions of the SNOMED CT terminology shows that the new method has overcome major drawbacks and limitations of existing methods, and has provided a feasible approach to the task of computing semantic di erence in large-scale ontologies.
In Computer Science & Arti cial Intelligence (AI), ontologies are a formal description of knowledge as a set of concepts within a domain and the relationships that hold between the concepts.
Since ontologies are dynamic entities that are constantly evolving, computing
the semantic di erence between two versions of ontologies can be a critical task:
to track what has changed in a new version of an ontology, to ensure that the
changes are safe in the sense of the new version being a conservative extension of
a preceding version [
A straightforward way to compute Diff(T1; T2) is to rst compute all logical entailments V2 of T2, and then collect from V2 the axioms not entailed by T1.
However, V2 can be in nite and computing V2 is not always computationally
feasible [
Existing UI methods are designed for DLs that are either more expressive or less expressive than real-world large-scale ontologies, which are often expressed in the DL E LH. This means that the computed views of the ontologies will contain language constructs that are outside of the language of E LH or they do not support language constructs of E LH. To be useful, views must be in the language of the input ontology and also satisfy the modeling guidelines of the development community.
Contributions. We introduce a novel, tailor-made UI method for the task of
computing semantic di erence for ontologies expressed in the DL E LH and as
large as SNOMED CT [
The source code, the long version of this paper and all test data are distributed at github.com/anonymous-ai-researcher/DL2021. User-friendly web access to try out these tools is possible at http://www.forgettingshow.info/. 2
Preliminaries Let NC and NR be disjoint and countably in nite sets of concept names and role names, respectively. E LH-concepts are inductively constructed based on the following syntax rule:
C; D
! > j A j C u D j 9r:C; where A 2 NC, r 2 NR, and C and D range over concepts. Let T be an E LHTBox and A; Bi 2 NC (1 i n) be atomic concepts in T . We say that A directly depends on B (A B) i the clausal form of T includes a clause in which A occurs positively and B negatively (or vice versa). We say that A depends on Bn i there is a chain of A, B1; : : : ; Bn such that A B1 : : : Bn. T is acyclic if there is no concept name in T that depends on itself; otherwise it is cyclic. In the remainder of this paper, the terms TBox and ontology are used interchangeably.
The semantics of E LH is de ned in terms of an interpretation I = h I ; I i, where I is the domain of the interpretation (a non-empty set), and I denotes the interpretation function, which assigns to every concept name A 2 NC a set AI I , and to every role name r 2 NR a binary relation rI I I . The interpretation function I is inductively extended to concepts as follows: A signature sig NC [ NR is a nite set of concept and role names. By sigC(X) and sigR(X) we denote the sets of respectively the concept names and role names occurring in X, where X ranges over concepts, axioms and ontologies. We let sig(X) = sigC(X) [ sigR(X). An axiom with S 2 sig( ) is called an S-axiom. De nition 1 (Semantic Di erence). Let T1 and T2 be two E LH-ontologies. Let be a subset of the shared signature of T1 and T2. The semantic di erence between T1 and T2 for is the set Diff (T1; T2) of all E LH-axioms such that (i) sig( ) , (ii) T2 j= , but (iii) T1 6j= . An axiom satisfying these conditions is a witness of a di erence in T2 w.r.t. T1.
We note that the witness set Diff (T1; T2) computes the information gain
from T1 to T2 and the information loss from T2 to T1 for the signature , where
sig(T1) \ sig(T2). To compute all witnesses in Diff (T1; T2) it is necessary to
compute all -entailments of T2 which are not entailed by T1. If Diff (T1; T2) 6= ;,
it is typically in nite and, therefore, cannot be presented to the user as such [
De nition 2 (Uniform Interpolation). Let T be an E LH-ontology. Let sig(T ) be a set of concept and role names. An E LH-ontology V is a -uniform interpolant of T i the following conditions hold: (i) sig(V) and (ii) for any E LH-axiom with sig( ) , V j= i T j= . In this case, the set is called the interpolation signature.
This means that uniform interpolants V have the same logical entailments as the given ontologies T up to , and thus are the strongest -entailments of T . The problem of semantic di erence can be related to that of UI as follows: Diff (T1; T2) = ; i T1 j= V2, where V2 is a -uniform interpolant of T2, for sig(T1) \ sig(T2). On the other hand, if T1 6j= V2, this means that Diff (T1; T2) 6= ;, and every 2 V2 with T1 6j= is a witness of Diff (T1; T2).
De nition 3 (UI-based Semantic Di erence). Let T1 and T2 be two E LHontologies. Let be a subset of the shared signature of T1 and T2. The UI semantic di erence between T1 and T2 is the set UI-Diff (T1; T2) of all E LHaxiom such that (i) sig( ) , (ii) 2 V2 and (iii) T1 6j= , where V2 is a -uniform interpolant of T2. An axiom satisfying these conditions is a UI-witness of a di erence in T2 w.r.t. T1.
Since any 2 V2 is a logical entailment of T2, every UI-witness is a witness and UI-Diff (T1; T2) Diff (T1; T2). Since all the witnesses can in principle be computed from the deductive closure of a -uniform interpolant V2 of T2, we can think of UI-Diff(T1; T2) as a representation of Diff(T1; T2). For E LH, UI-Diff(T1; T2) is a nite representation of Diff(T1; T2). It follows from these considerations that the set UI-Diff(T1; T2) of UI-witnesses can be computed using the following algorithm: -uniform interpolant V2 of T2, for sig(T1) \ Step (1): compute the
sig(T2), and then Step (2): collect the axioms
2 V2 not entailed by T1.
The rst step can be done using a UI method/tool, and the second step can be done using an external DL reasoner. 3
Limitations of Existing Uniform Interpolation Methods
A few methods have been developed for various DLs. These methods include
NUI [
NUI [
LETHE, UI-FAME, as well as the method of [
The evaluations in [
A Novel UI Method for E LH In this section we introduce a tailor-made method for computing uniform interpolants of E LH-ontologies for Step (1). In particular, we develop a new method for forgetting concept and role names from E LH-ontologies. 4 SNOMED CT used to be an acyclic ELH-terminology, but began to include GCIs from its International 2019 January release.
Central to the forgetting method are two mutually independent calculi, namely a calculus for concept name elimination and a calculus for role name elimination. The process of computing uniform interpolants is to rstly deal with concept forgetting, then role forgetting, then treat introduced de ners as regular concept names to carry out forgetting. In the remainder of this paper, we refer to the concept or role name under current consideration for forgetting as the pivot. The notation and F is uniformly used to denote the interpolation signature and the forgetting signature, respectively. Let T denote an E LH-ontology. 4.1
Let A 2 sigC(T ) be the pivot concept. The calculus for eliminating A from T includes two steps that are executed in sequence. The rst step is to transform T into A-reduced form (normalization), which is a specialized normal form to which some of the inference rules in the calculus (presented later) are applicable. The second step is to apply these inference rules to T to eliminate A. De nition 4 (A-Reduced Form). An E LH GCI is in A-reduced form if it has one of the following forms, where (i) r; s 2 NR, (ii) C, D, E and F are concepts not containing A, (iii) G 6= A is an atomic concept or a concept of the form 9r:X for X a concept not containing A. An E LH-ontology T is in Areduced form if every A-axiom in T is a GCI in positive or negative A-reduced form.
I: C v A
II: C v 9r:(A u D) III: A u F v G
IV: 9s:(A u E) u F v G
Given any E LH-ontology T , one can compute in polynomial time an equisatis able E LH-ontology in A-reduced form by applying exhaustively the following rules to the A-axioms in T : 1. replace each C C1 with C v C1 and C1 v C; 2. replace each C v C1 u C2 with C v C1 and C v C2; 3. if 9s:C occurs somewhere on the left-hand side of a GCI in T , where s 2 NR and C is a concept containing A, replace C with a fresh concept name X 2 NC and add C v X to T ; 4. if 9s:C occurs somewhere on the right-hand side of a GCI in T , where s 2 NR and C is a concept containing A, replace C with a fresh concept name X 2 NC and add X v C to T ; 5. if A occurs in Z, where Z is a placeholder for the concept \C", \E", or \F " in the above A-reduced form, replace Z with a fresh concept name X 2 NC and add Z v X to T ; 6. if A occurs in Z, where Z is a placeholder for the concept \D" or \G"in the above A-reduced form, replace Z with a fresh concept name X 2 NC and add X v Z to T .
The fresh concept names X 2 NC introduced in the above rules are called
de ner names or simply de ners [
Lemma 1. For any E LH-ontology T , one can construct in polynomial time a normalized E LH-ontology T 0 of polynomial size in jT j such that (i) sig(T ) sig(T 0) and (ii) T 0 j= T , and for every model I of T there exists a model J of T 0 such that I = J and XI = XJ for every X 2 sig(T ). T 0 is acyclic if T is acyclic.
Lemma 1 states that de ner introduction preserves the underlying logical
models of the concepts and roles in the original axioms (De nition 2 holds).
Normalized E LH-ontologies in this sense are modi cations of normalized
terminologies as de ned by [
a. C v A; A u F v G =) C u F v G b. C v A; 9s:(A u E) u F v G =) 9s:(C u E) u F v G c. C v 9r:(A u D); A u F1 v G1; : : : ; A u Fn v Gn c. =) C v 9r:(G1 u : : : u Gn u D) c. provided that: Fi i n
> for 1 c. C v 9r:(A u D); A u F v G1; : : : ; A u F v Gn c. =) C v 9r:D; C v 9r:(G1 u : : : u Gn) c. provided that: F 6 > and T j= D v F c. C v 9r:(A u D); A u F v G =) C v 9r:D c. provided that: T 6j= D v F d. C v 9r:(A u D); 9s:(A u E) u F v G d: =) C v 9r:D; C u F v G d. provided that: T j= D v E and T j= r v s d. C v 9r:(A u D); 9s:(A u E) u F v G =) C v 9r:D d. provided that: T 6j= D v E or T 6j= r v s
Once T is in A-reduced form, the second step is to eliminate A from T using the inference rules shown in Figure 1. The elimination of A is based on an exhaustive application of the inference rules to all (reduced) A-axioms in T to derive new logical entailments on A (and add them to T ) until T is saturated w.r.t. A, and then remove all A-axioms from T . Inferences to reveal logical entailments of a name is often based on combining positive and negative occurrences of the name, which is also re ected in the inference rules of this calculus. In the context of forgetting, ontologies are assumed to be consistent, so no contradiction would be derived. Also, termination is guaranteed because A do not occur in newly-derived entailments, meaning that there would be no recursive derivations and saturation can be reached in nite steps.
Speci cally, Rule (a) and Rule (b) combines each GCI of Form I, which contains a positive occurrence of A, with each GCI of Form III and Form IV, respectively, which contain a negative occurrence of A; Rule (c) and Rule (d) combines each GCI of Form II, which contains a positive occurrence of A, with each GCI of Form III and Form IV, respectively.
Lemma 2. The calculus for concept name elimination is sound. Proof (sketch). To prove that the calculus is sound is to prove that the output OU T of the calculus has the same logical entailments as its input IN up to the signature sig(IN )nfAg.
The calculus for concept name elimination includes the normalization step
and the inference step, so its soundness follows from the rules used in both steps.
The rst two normalization rules are standard transformations preserving logical
equivalence. The latter four normalization rules are the structural
transformation [
Let r 2 sigR(T ) be the pivot role name. The calculus for role name elimination, as with that for concept name elimination, includes two steps executed in sequence. The rst step is to transform T into another specialized normal form, namely rreduced form, which generalizes all elementary forms of a concept/role inclusion where a role name r could occur.
De nition 5 (r-Reduced Form). An inclusion is in r-reduced form if it has one of the following forms, where (i) s; r 2 NR, (ii) C, E, F , D and G are concepts not containing r. An E LH ontology T is in r-reduced form if every r-axiom in T is an inclusion in r-reduced form.
I: s v r
II: C v 9r:D
III: r v t IV: F u 9r:E v G
Observe that an r-role inclusion is naturally in r-reduced form. r-clauses not in r-reduced form can be transformed into the form by a trivial adaptation of the de ner introduction for concept elimination, which inherits all its properties including Lemma 1.
e. s v r; r v t =) s v t f. s v r; F u 9r:E v G =) F u 9s:E v G g. C v 9r:D; r v t =) C v 9t:D h. C v 9r:D; F u 9r:E v G =) F u C v G h: provided that: T j= D v E
Once T is in r-reduced form, the second step is to apply exhaustively the inference rules shown in Figure 2 to eliminate r from T . The idea is analogous to that in concept name elimination, that is, to derive from the r-axioms all logical entailments not involving r, add them to T , and then remove from T the r-axioms.
Lemma 3. The calculus for role name elimination is sound.
Proof (sketch). The rst three inferences rules are generalizations of Ackermann's
Lemma which preserve equivalence up to the interpolation signature. The last
rule can be solved using unfolding [
Theorem 1. For any E LH-ontology T and an interpolation signature sig(T ), our UI method always terminates and returns an E LH ontology V. If V does not contain any de ners, then our method succeeds and V is a -uniform interpolant of T . For any acyclic E LH-ontology T and a signature sig(T ), our method always terminates and returns a -uniform interpolant V of T . To understand the practicality of our UI method, we implemented a prototype in Java using the OWL API Version 3.5.7,5 and compared it with LETHE on a corpus of real-world ontologies.
We selected 488 ontologies from the Oxford ISG6 snapshot with the size jOntoj of TBox axioms not exceeding 10000. We further split the 488 ontologies into three subparts: PART I with 10 jOntoj < 1000, containing 355 ontologies, PART II with 1000 jOntoj < 5000, containing 108 ontologies, and PART III with 5000 jOntoj 10000, containing 25 ontologies. This would provide clear clues for better understanding of the performance of our UI method for realistic ontologies of di erent size ranges. The selected ontologies were restricted to their E LH-fragments by removing from them those axioms not expressible in E LH. On average 8.9% of the axioms were thus dropped from the ontologies. Statistical information about the adapted ontologies is shown in Table 1. We repeat the tests three times for each ontology.
To t with real-world applications, the experiments were conducted for two settings: forgetting respectively 10% and 30% of the concept and role names in the signature of each ontology. The forgetting signature was randomly chosen. The experiments were conducted on a laptop with an Intel Core i7-9750H processor, 6 cores running at up to 2.70 GHz, and 12 GB of DDR4-1600 MHz RAM. The timeout was limited to 300 seconds and heap space to 9GB.
The success for forgetting was de ned as: (i) eliminating all the names in F , (ii) not leaving any de ners in the solutions, (iii) nished in the time and space limit. The results, shown in Table 2, are quite revealing in several ways. The most encouraging result is that our UI prototype succeeded in almost all test cases, and in most of these successful cases the forgetting was nished in an instant. In particular, compared to LETHE, our prototype fared considerably better w.r.t. success rates. Failures of our prototype were due to cyclic dependencies (over the names in F ) being present in the original ontologies and the timeout. Most
6 http://krr-nas.cs.ox.ac.uk/ontologies/lib/
LETHE
Our Prototype
failures of LETHE were due to timeout. Our prototype outperformed LETHE
in speed performance, and was at least ve to ten times faster than LETHE.
We conjecture (also evidenced by the results of memory consumption) this is
most likely because LETHE uses an expensive de ner introduction algorithm to
atten complex clauses, where the number of introduced de ners is bounded by
O(2n), for n the number of input clauses [
The best way to verify our conjecture was to track the working process of LETHE but this was infeasible due to the unavailability of the source of LETHE. We then designed an alternative experiment; see Figure 3. In the Cartesian coordinate system, the x-axis denotes the number of GCIs in a test ontology fragment (e.g., the number of A-clauses when forgetting A), which re ects the size of the fragment, and the y-axis denotes the number of de ners our UI prototype introduced in a test case, which re ects the atness of the test ontology. Less de ners normally came with atter ontologies. The blue points mark the cases where our UI tool succeeded but LETHE failed. The orange points mark those where both succeeded. Now it is clear that the size of ontologies was not a problem for LETHE, but a complex internal structure with a large number of de ners in demand for normalization would increase the probability of failure for LETHE. 6
Case Studies SNOMED CT is presently the most comprehensive, multilingual clinical healthcare ontology in the world, and has been integrated into the knowledge base of many e-health vendors. SNOMED International7 owns and maintains SNOMED
CT on an ongoing basis, issuing releases of its International Edition at the end
of January and July each year. In this section we studied how our UI method
performs in practice for the task of tracking the semantic evolutionary changes
in di erent versions of SNOMED CT. We computed the semantic di erence
between 15 consecutive international releases of SNOMED CT, as well as 5
nonconsecutive international releases using a UI-Diff tool that employed our UI tool
to perform Step (1) and the DL reasoner HermiT [
Figure 4, where the x axis denotes di erent SNOMED CT versions combinations of which we want to compute semantic di erence (1601 denotes 2016 January release, others are in a same way), and the y axis denotes the number of axioms, re ects the semantic changes over the evolution of the International SNOMED CT edition, i.e., the information gain UI-Diff (T ; T 0) and the information loss UI-Diff (T 0; T ), where = sig(T ) \ sig(T 0). With the UI-witness set being successfully generated in all of the 20 comparison cases, our UI tool demonstrated superb performance for forgetting. Table 3 summarizes the metrics of the forgetting task corresponding to each comparison case, where jFCj and jFRj denote respectively the number of concept and role names to be forgotten, j v j the number of axioms in the given normalized ontology, and T(s) the time duration for forgetting. To the best of our knowledge, our UI prototype is so far the only tool capable of forgetting 10K+ number of concepts and roles from ontologies as large as containing 600K+ logical statements. All forgetting tasks were nished within a reasonable period of time. This provides ontology engineers with a powerful tooling support to create views of industrial-scale ontologies. 7
Conclusion and Future Work We developed a novel, tailor-made UI method. On a large corpus of adapted Oxford ISG ontologies, our UI method has shown superb performance and superiority over LETHE (the state-of-the-art UI tool) by a large margin. Case studies on di erent versions of SNOMED CT have veri ed the viability of our semantic di erence algorithm as back-end technology in e-health vendors' knowledge base interface for their main concerns of content analysis and quality assurance.
An immediate future step is to nd justi cations [