We implement and evaluate a recently introduced method to compute uniform interpolants for ontologies speci ed in the description logic ALC. The aim of uniform interpolation is to reformulate an ontology such that it only uses a speci ed set of symbols, while preserving consequences that involve these symbols. Uniform interpolation is useful to applications in ontology engineering and modular ontologies. It is known that uniform interpolants of ontologies in ALC cannot always be presented in a nite way, and that their size can in the worst case be triple exponential in the size of the original ontology. These properties leave the question on how practical computing uniform interpolants is. The aim of this paper is to approach this question by implementing our recently presented method that always computes a nite representation of the uniform interpolant { either by using xpoint logics or by extending the signature { and by undertaking an experimental evaluation of the method on a larger set of real-life ontologies.
Ontologies represent information about concepts and relations (roles) using description logics, fragments of rst-order logic, to allow reasoning systems to derive implicit information automatically. The signature of an ontology is the set of symbols used by the ontology. In forgetting, the aim is to remove concept or role symbols from an ontology in such a way that all logical consequences over the remaining symbols are preserved. The result of forgetting is a uniform interpolant, the original ontology restricted to a smaller signature, such that all consequences over that signature are preserved.
Uniform interpolation and forgetting have several potential applications that
are interesting in the context of ontology engineering and modular ontologies.
For example, an ontology to be published contains con dential parts that should
not be accessible by the public. A solution to this problem is predicate hiding [
Other applications aim at analysing ontologies or ontology changes. One such application is exhibiting hidden relations. Often relations between di erent concepts are not stated explicitly but are only deducible with the help of reasoners. To get a better understanding how certain concepts relate to each other, one can compute the uniform interpolant over a signature of interest. Uniform interpolation can also be used to compute the logical di erence between two versions of an ontology. Extending or modifying an ontology can lead to unintended results. Checking whether consequences over a speci ed signature are preserved in a new version can be performed by computing its uniform interpolant and testing whether it is entailed by the original ontology.
Despite these applications, there has not been much work yet to develop
practical algorithms for uniform interpolation on real-life ontologies in expressive
description logics. A reason for this might be that the known theoretical
properties of uniform interpolation cast doubt on whether such practical methods even
exist: it is known that for ontologies expressed in ALC, uniform interpolants
are not always expressible in a nite way, if ALC is also used to represent the
uniform interpolant. Also, in the worst case, the size of the uniform interpolant
can be triple exponential in the size of the original ontology [
In [
In order to approach the question as to whether the method is also practical for the mentioned applications, we present an experimental evaluation of the method on real life ontologies. The results suggests that, while for some ontologies uniform interpolants are still hard to compute, there are a lot real-world cases for which the method can be used. 2
Let Nc, Nr be two disjoint sets of concept symbols and role symbols. Concepts in ALC are of the following form:
? j > j A j :C j C t D j C u D j 9r:C j 8r:C; where A 2 Nc, r 2 Nr and C and D are arbitrary concepts. >, C u D and 8r:C are de ned as abbreviations: > stands for :?, C u D for :(:C t :D) and 8r:C for :9r::C.
A TBox is a set of axioms of the forms C v D and C D, where C and D are concepts. C D is a short-hand for the two axioms C v D and D v C. Since we are only dealing with the TBox part of an ontology, we will use the terms `ontology' and `TBox' interchangeably.
We write C[A] to denote a concept that contains a concept symbol A, and denote the result of replacing A by a di erent expression E by C[E]. For a TBox T , T [A7!C] denotes the result of replacing every A in T by C.
The semantics of ALC is de ned as follows. An interpretation is a pair I = h I ; I i, where the domain I is a nonempty set and the interpretation function I assigns to each concept symbol A 2 Nc a subset of I and to each role symbol r 2 Nr a subset of I I . The interpretation function is extended to concepts as follows: ?I := ; (:C)I :=
I n CI (C t D)I := CI [ DI (9r:C)I := fx 2
I j 9y : (x; y) 2 rI ^ y 2 CI g: C v D is true in an interpretation I i CI DI . I is model of a TBox T if all axioms in T are true in I. A TBox T is satis able if there exists a model for T , otherwise it is unsatis able. T j= C v D holds i in every model of T we have CI DI .
In order to de ne ALC , we extend the language with a set Nv of concept variables. ALC extends ALC with concepts of the form X:C and X:C, where X 2 Nv, and C is a concept in which X occurs as a concept symbol only positively (under an even number of negations). X:C is the least xpoint of C on X, X:C the greatest xpoint.
A concept variable X is bound if it occurs in the scope C of a xpoint expression X:C or X:C. Otherwise it is free. A concept is closed if it does not contain any free variables. Axioms in ALC are of the form C v D and C D, where C and D are closed concepts.
Following [
I j CI;V[X7!W ]
W g I j W
CI;V[X7!W ]g:
A signature is a subset of Ns [ Nr. sig(E) denotes the concept and role
symbols occurring in E, where E ranges over concept descriptions, axioms and
TBoxes. Given two TBoxes T1, T2 and a signature , we say T1 and T2 are
-inseparable, in symbols T1 T2, i for every concept inclusion with
sig( ) , T1 j= implies T2 j= and vice versa. Given a TBox T and a
signature , T 0 is a uniform interpolant of T if sig(T 0) and T T 0(Note
that in contrast to conservative extensions and deductive modules no syntactical
constraints are given[
In the following we give a brief overview of our method for computing uniform
interpolants. For a more detailed description see [
Given a TBox T , the clausal form of T , denoted by clauses(T ), is a TBox T 0 with T sig(T ) T 0, such that every axiom is of the form > v L0 t ::: t Ln, where every Li is of the form A,:A, 9r:D or 8r:D, with A 2 Nc, r 2 Nr and D 2 ND. ND Nc n sig(T ) is a set of designated concept symbols called de ner symbols. Any TBox can be transformed into its clausal form using standard structural transformation and conjunctive normal form transformation techniques. We will refer to axioms of a clausal form TBox as clauses and just write L0 t ::: t Ln omitting the leading > v. We also assume that clauses are represented as sets (that is, no disjunct occurs twice in a clause and the order of the disjuncts does not matter).
Our method to compute T A consists of ve phases: 1. Set N =clauses(T ). 2. Saturate N using the rules in Figure 1. 3. Filter out unnecessary clauses and group clauses of the form :D t Ci, where
D 2 ND, into concept inclusions D v d Ci.
C1 t B
C2 t :B
C1 t C2 where B is the symbol A we want to forget or a de ner symbol and provided C1 t C2 does not contain more than one negative de ner literal.
Role Propagation:
C1 t 8r:D1
C2 t Qr:D2
C1 t C2 t Qr:D3 where Q 2 f9; 8g and D3 is a (possibly new) de ner symbol representing D1 u D2 and provided C1 t C2 does not contain more than one negative de ner literal. 4. Apply the rules in Figure 2 exhaustively to eliminate introduced symbols. 5. Apply simpli cations and represent clauses as proper concept inclusions.
The rules in Figure 1 derive all consequences based on the selected concept symbol A we want to eliminate, rendering clauses containing A super uous for the uniform interpolant. The role propagation rule is special since it may involve the introduction of new de ner symbols. Because we want to preserve the clausal form in Phase 2, in order to represent a concept conjunction D1 u D2, we introduce a new de ner symbol D3 and add two clauses :D3 t D1 and :D3 t D2 to the current clause set. In order to restrict the introduction of new de ner symbols, we keep track of each introduced de ner symbol and reuse them as much as possible. By doing this wisely it is possible to restrict the number of introduced de ner symbols to maximally 2jNDj.
It can be shown that if a set of clauses is saturated using the rules in Figure 1,
all clauses containing the selected concept symbol A and all clauses containing
positive de ner symbols that do not occur under a role restriction can be
removed, and the resulting set is still -inseparable with the original TBox [
If the desired target language is ALC, the cyclic de ner elimination rule cannot be applied, since it introduces xpoint operators. In this case the cyclic de ners remain in the result, which means the resulting TBox is not a uniform interpolant. It does, however, not contain A and preserves all consequences not containing A. The remaining cyclic de ners can be seen as `helper concept symbols' that help keep the result nite without using xpoint operators. The result of applying only non-cyclic de ner elimination and de ner puri cation can be viewed as signature-wise approximation of the uniform interpolant. It should be noted though that the existence of cyclic de ners in the returned result does not necessarily imply that there is no nite representation of the uniform interpolant in ALC.
In [
We implemented our forgetting method in Scala1 using the OWL API.2 Since xpoint operators are not supported by most standards and reasoners, for practical applications it is of interest to compute only results that are expressible in ALC. For this reason, our method does not eliminate de ner symbols where this would lead to a xpoint operator in the result. In order to make the method practical, we implemented several optimisations.
Restricting the Role Propagation Rule. Though in its presented form the calculus works correctly, in order to make the method practical, it is neccessary to apply further restrictions on the role propagation rule. The main role of the role propagation rule is to derive new clauses between which resolution on the symbol we want to forget is applicable. In order to avoid the unnecessary introduction of new clauses and de ner symbols, we check beforehand whether applying role propagation contributes to any further resolution rule applications. If not, we omit its application.
Redundancy Elimination. From the proofs in [
Structural Transformation. Since the resolution rule and the role
propagation rule only apply to a restricted subset of literals in the clause set, the
number of clauses can be signi cantly reduced by using further structural
transformations. For a clause C, let CA denote the literals on which our rules apply,
and CA the remaining literals. We replace each set of clauses fC0; :::; Cng, such
that CA = CjA for all i; j < n, by a single clause X t C0A, where X is a new
i
concept symbol, and store the information that X C0A u ::: u CnA. As soon as
a clause is added to the result set, we undo this transformation and apply eager
subsumption deletion on the current result set. This optimisation is in uenced
by the uniform interpolation method presented in [
Simpli cations. The simpli cations performed in Phase 5 are the following. Following an arbitrary ordering de ned on concept symbols, we select the maximal literal of the form :A, if existent, and transform the clause into an axiom of the form A v C. We then group all concept inclusion axioms that have the same concept A on the right hand side into a single concept inclusion. We apply several replacement rules to remove tautological or unsatis able subexpressions. We also detect tautological xpoint-expressions. For any xpoint expression X:C[X], if C[>] is a tautology, > is the greatest xpoint of C[X], and we can replace X:C[X] by >. Tautological and unsatis able sub-expressions are detected using sound but incomplete syntactic criteria. Since the number of introduced de ner symbols can be exponential in the number of role restrictions of the input ontology, it is also wise to minimise their occurrences. This is accomplished in Phase 5 by transforming disjunctions of the form 9r:C0 t ::: t 9r:Cn into single existential role restrictions 9r:(C0 t ::: t Cn) and conjunctions of the form 8r:C0 u ::: u 8r:Cn into single universal role restrictions 8r:(C0 u ::: u Cn).
Module extraction. To restrict the number of symbols we have to forget,
we rst extract the syntactic locality based >? -module [
Puri cation. Before applying our method, we compute the negation normal form TNNF of the input ontology T . If a concept symbol A occurs only positively in TNNF , then T A = T [A7!>]. If A occurs only negatively in TNNF , then T A = T [A7!?]. We call this transformation puri cation of A. The soundness of puri cation follows from the fact that in these cases the resolution rule would never be applied, what e ectively means we only remove clauses containing A. Puri cation of A leads to an equivalent result as removing clauses containing A, but can be performed much faster. When computing uniform interpolants for our experimental evaluation, we observed that in some cases already thousands of concept symbols could be eliminated using puri cation.
In order to evaluate how our implementation behaves on real-life ontologies,
we selected a set of ontologies from the NCBO BioPortal ontology repository.3
The ontologies of this corpus are known to be diverse in complexity, size and
structure [
Since our method is designed for ALC-ontologies, we restricted the ontologies to their ALC-fragments in the following way. Axioms that can be rewritten into ALC axioms in a uni ed way (equivalent concepts, disjoint concepts, disjoint union axioms, property range axioms and property domain axioms) were rewritten, the remaining axioms that are not in ALC were removed from the TBox. We further removed all ontologies where the ALC-fragment of the TBox contained less than 5 concept symbols or consisted only of axioms of the form A v B and A B, where A and B are concept symbols. This way, we extracted a corpus of 207 ontologies for our experiments.
In these ontologies, on average 5.75% of the TBox axioms had to be removed in order to generate an ALC-TBox, while 54 ontologies were completely expressible in ALC.
The ontologies of the resulting corpus contain between 2 and 187,514 concept symbols (on average 5,728). The average number of axioms per ontology is 21,821.20 and the average axiom size is 4.61. The size of an axiom is de ned recursively as follows: size(A) = 1, where A is a concept symbol, size(:C) = size(C) + 1, size(9r:C) = size(8r:C) = size(C) + 2, size(C t D) = size(C u D) = size(C) + size(D) + 1, and size(C v D) = size(C D) = size(C) + size(D) + 1.
The experiments were run on an Intel Core i5-2400 CPU with four cores running at 3.10 GHz and 8 GB of RAM. Since our implementation does not make use of multi-threading, we ran several experiments in parallel in order to make full use of the multiple processors.
Depending on the application, it might either be interesting to forget a small set of concept symbols from the ontology (predicate hiding, ontology obfuscation, logical di erence), or to restrict the ontology to a small signature (exhibit hidden relations, sharing restricted parts of an ontology). We rst considered how our method performed on forgetting small sets of concept symbols. For this we selected random subsets of 5, 10, 50 and 150 concept symbols, 10 subsets in each case, from the signature of each ontology, for which we applied our method. Since the average number of concept symbols per ontology is 5,728, in most cases this represented a small subset of the overall signature. If, however, the signature of an ontology contained less than the selected number of concept symbols, we omitted the corresponding experiments. This was the case for 4, 21 and 60 ontologies for the signature sizes 10, 50 and 150, respectively. 3 http://bioportal.bioontology.org 8000 7000 s n uR 6000 l a t en 5000 m i rep 4000 x E fo 3000 r e bm 2000 u N 1000 0 1 10 100
1000
Time (sec.) Ontologies jsig(T ) n j Timeouts De ners Left AovfeAraxgieomNsr. AovferAaxgieomSisze DAuvreartaigoen All NCI
We used a timeout of 1,000 seconds for each experimental run. In order to evaluate how our method performed on larger ontologies, we applied the same procedure on the ALC-fragment of Version 13.05d of the National Cancer Institute Thesaurus (NCI), which was part of our corpus. The ALC-fragment of this ontology, represented only using the operators presented in the Preliminaries Section, has 138,260 axioms of average size 5. Here, we set a higher timeout of an hour, as well as higher numbers of concept symbols, and performed 100 runs for each number.
The size of the ontologies remained mostly unchanged, which was due to the fact that a major part of the ontology was not touched by the method if the concept symbols were only used in a small subset.
With an increasing number of forgotten concept symbols the number of cases in which de ner symbols are left in the result rose slightly, but in 93% of the cases the result could be represented nitely without de ner symbols. In 99% of the cases our method was able to compute the forgetting result in the set time limit. The average duration suggests that a much smaller timeout could already have led to similar results. Figure 3 shows the cumulative distribution of the durations of each experimental run. It shows that nearly 6,000 out of 7,426 experimental runs could be performed within less than one second, which suggests that for most cases, forgetting small sets of concepts is actually a cheap operation.
Next we wanted to evaluate how good our method performed on restricting the signature of an ontology to a small set of concept symbols. Since computing uniform interpolants for small signatures is much more computationally expensive as forgetting small sets of concept symbols, we performed the experiments only on a subset of the original corpus, for which we randomly selected 170 ontologies, and performed 5 experimental runs for each ontology and sample size. The results are summarised in Table 2.
The e ect of uniform interpolation was more apparent in these cases. In 20.1% of the cases, the computed uniform interpolant would have used xpoint operators. Even if only 5 concept symbols were used in the result, the average axiom size was 627. In case of the NCI ontology, the average size of an axiom was even higher. The main reason for this is that much more information about the role structure of the ontology and disjointnesses between concepts had to be represented in fewer axioms.
Figure 4 plots the sizes of input ontologies and the sizes of the extracted modules against the sizes of the signature-wise approximated uniform interpolants. Interestingly, in most cases the computed uniform interpolant was of similar size or smaller than the corresponding module. In 90.0% of the cases, the resulting ontology was smaller than the input ontology, and in 75.9% of the cases, it was smaller than the corresponding >? -module. In the most extreme case the uniform interpolant was however 559 times bigger than the corresponding >? -module.
The performance on our method strongly depended on how distributed the concept symbols to be forgotten are in the ontology, and how many additional symbols remained in the module. The biggest e ect on computation time and output size was caused if the concept symbols to be forgotten occurred in high numbers nested under role restrictions, since the role propagation rule had to be applied more often in these cases. This lead to a high number of clauses and seemed to be the main cause for timeouts.
The corpora used for the experiments, as well as the implementation, can be found under http://www.cs.man.ac.uk/~koopmanp/womo_experiments. 6
We implemented and evaluated a recently presented method to compute uniform interpolants of ALC-ontologies. Uniform interpolation has a lot of potential applications in ontology engineering and modular ontologies. It is known that uniform interpolants of ALC-ontologies cannot always be represented in a nite way in ALC, and their size is in the worst case triple exponential in the size of the input ontology. We evaluated an implementation of uniform interpolation to investigate how these theoretical properties a ect uniform interpolation of ALCfragments of real-life ontologies. Our method computes uniform interpolants for ALC , which is ALC extended with xpoint operators, to enable the nite representation of uniform interpolants in all cases. Since xpoint operators are not supported by most standards and reasoners, our implementation uses helper concept symbols in the result, which means the computed ontologies approximate the uniform interpolant signature-wise. Our experiments showed however, that in a majority of cases this was not needed, since the uniform interpolant could be represented without xpoint operators. Our experiments suggest that, even though the worst case complexity of the size of uniform interpolants is triple exponential, in reality, the situation where the interpolant is exponential rarely occurs. In fact, in most cases uniform interpolants could be computed in a few seconds, and were even smaller than the input ontologies. These results suggest that, even though computing uniform interpolation for complex ontologies can be expensive, there are a lot of applications where it is practical.
In contrast to the earlier approaches on uniform interpolation of ALC-ontologies
presented [