We present a method to compute uniform interpolants of ALC-ontologies with ABoxes. Uniform interpolants are restricted views of ontologies that only use a speci ed set of symbols, but share all entailments in that signature with the original ontology. This way, it allows to select or remove information from an ontology based on a signature, which has applications in privacy, ontology analysis and ontology reuse. We show that in general, uniform interpolants of ALC-ontologies with ABoxes may require disjunctive statements or nominals in the ABox. An evaluation of the method suggests however, that in most practical cases uniform interpolants can be represented as a classical ALC-ontology.
We present a method to compute uniform interpolants of ALC-ontologies with ABoxes. Modern applications, especially in bio-informatics or medical domains, often demand ontologies that cover a large vocabulary. With rising complexity, these ontologies become harder to maintain and modify. Uniform interpolation and forgetting deal with the problem of reducing the vocabulary used in an ontology in such a way that all entailments over the reduced vocabulary are preserved. In contrast to modules, uniform interpolants are completely in the desired signature and may contain di erent axioms than the input ontology.
There are a range of applications for uniform interpolation. One can use it
to extract a part of an ontology for reuse, if only a subset of the terms de ned
in the ontology is interesting for an application [21]. It also provides a way to
remove con dential information from an ontology to be shared among users with
di erent privileges [
Uniform interpolation of TBoxes has been extensively studied in the
description logic literature [
ALC-uniform interpolants preserve all entailments of the form C v D, C(a)
and r(a; b), where C, D and r are ALC-concepts and roles that only use
concept and role symbols from a speci ed signature. As it turns out, traditional
ALC-ontologies are not always su cient to represent uniform interpolants that
preserve all these entailments. It is already known that cyclic de nitions in the
TBox may require the use of xpoint operators or additional symbols in the
uniform interpolant [
To illustrate this, take as an example the ontology O containing the TBox axiom A v 8r:(:B t A) and the ABox assertions r(a; b), r(b; a) and B(b). The ALC-uniform interpolant of this ontology for = fA; rg has to preserve all ALC-entailments that only use A and r. This is the case for the ABox A = fr(a; b); r(b; a); :A(a) _ A(b)g. A is therefore an ALC-uniform interpolant of O for . We can replace the disjunction in this ABox by the ALCO-concept assertion (:A t 9r:(fbg u A))(a). But in this case, it is impossible to preserve all entailments of O in an ALC-ontology without disjunctions in the ABox. Our evaluation suggests however, that in most practical cases uniform interpolants can be represented without nominals or disjunctions.
In the next section we present the description logics used in this paper, and
give a formal de nition of uniform interpolation. In Section 3, we describe a
method based on a new resolution calculus that is used to compute a clausal
representation of the uniform interpolant. The method introduces new symbols
to the signature, as well as disjunctions of concept assertions. In Section 4 we
describe how these introduced symbols are eliminated and how a uniform
interpolant without disjunctions can be computed. The result may contain xpoints
and nominals. Since xpoints are not commonly supported by current
description logic reasoners, we describe how uniform interpolants can be represented
in ALC, respectively ALCO, by either using additional symbols or
approximating the uniform interpolant. We evaluate our method in Section 5 and give an
overview of related work in Section 6. We conclude with a short conclusion
in Section 7. Proofs of all lemmas and theorems can be found in the long version
of this paper [
We present the description logics ALC, ALC , ALCO and ALCO , and give a formal de nition of disjunctive ABoxes and uniform interpolants.
Let Nc, Nr, Ni and Nv be four disjoint sets of respectively concept symbols, role symbols, individuals and concept variables. ALCO -concepts are of the form >, A, :C, C t D, 9r:C, fag and X:C[X], where A 2 Nc, r 2 Nr, a 2 Ni, X 2 Nv, C and D are ALCO -concepts and C[X] is an ALCO -concept in which X occurs positively (under an even number of negations) as a replacement for a concept symbol. We de ne further concepts as abbrevations: ? = :>, C u D = :(:C t :D), 8r:C = :9r::C, X:C[X] = : X::C[:X] and fa1; :::; ang = fa1g t : : : t fang. X:C[X] denotes the least xpoint of C[X] and X:C[X] the greatest xpoint.
A TBox T is a set of axioms, which are either concept inclusions C v D or concept equivalence axioms C D, where C and D are ALCO -concepts. An ABox A is a set of concept assertions C(a) and role assertions r(a; b), where r 2 Nr, a; b 2 Ni and C is any ALCO -concept. An ontology O is a tuple hT ; Ai, where T is a TBox and A is an ABox. If an ontology does not contain xpoint expressions X:C[X] or X:C[X], it is an ALCO-ontology. If it does not contain nominal expressions fag or fa1; :::; ang, it is an ALC -ontology. If it contains neither nominals nor xpoint expressions, it is in an ALC-ontology. In the same way, we de ne ALC (ALCO, ALC ) -axioms, -concepts and -assertions.
The semantics is de ned as usual (see, e.g., [
A disjunctive concept assertion is of the form C1(a1) _ : : : _ Cn(an), where the Ci are ALCO -concepts and the ai individuals, 1 i n. Given an ontology O, let Oj=C1(a1) _ : : : _ Cn(an) i O j= Ci(ai) for at least one 1 i n. A disjunctive ABox is a set of role assertions, concept assertions and disjunctive concept assertions. To make the distinction clear, we refer to ABoxes which do not contain disjunctive concept assertions as classical ABoxes.
A signature (Nc [ Nr) is a set of concept and role symbols. Given a concept, axiom, assertion, TBox, ABox or ontology E, the signature of E, denoted by sig(E), is the set of concept and role symbols occurring in E. Given an ontology O and a signature , O is an ALC-uniform interpolant of O for , i (i) sig(O ) and (ii) O j= i O j= for every ALC-axiom and nondisjunctive ALC-assertion with sig( ) . Since we do not de ne any other kinds of uniform interpolants, we refer to ALC-uniform interpolants simply as uniform interpolants in the remainder of this paper. Note that we do not require ALC-uniform interpolants to be expressed in ALC itself. We just require them to preserve all entailments that can be expressed in ALC.
If = sig(O) n fxg, where x is a single concept or role symbol, we call the uniform interpolant O the result of forgetting x from O, and denote it by O x. 3
The method for computing uniform interpolants works on a clausal form of the input ontology, which uses an additional set of special concept symbols. De nition 1. Let Nd Nc be a set of designated concept symbols called deners. A TBox literal is a concept of the form A, :A, 9r:D or 8r:D, where A 2 Nc and r 2 Nr and D 2 Nd. A TBox clause is a concept inclusion of the form > v L1 t : : : t Ln, where each Li is a TBox literal. An ABox literal is a concept assertion of the form L(a), where L is a TBox literal and a 2 Ni. An ABox clause is a disjunctive concept assertion of the form L1 _ : : : _ Ln, TBox Resolution:
C1 t A provided C1 [ C2 does not contain more than one negative de ner-literal. TBox Role Propagation:
C1 t 8r:D1 C2 t Qr:D2
C1 t C2 t Qr:D12 where Q 2 f9; 8g and D12 is a (possibly new) de ner representing D1 u D2, provided C1 [ C2 does not contain more than one negative de ner-literal. TBox Existential Role Restriction Elimination: C t 9R:D
C
:D where every Li is an ABox literal. An ontology is in clausal form if its TBox consists only of TBox clauses and its ABox consists only of ABox clauses and role assertions.
We omit the leading '> v' in TBox clauses and assume that every clause is represented as a set. This means, no literal appears twice in a clause and the order of the literals is not important. Every ontology can be transformed into clausal form using standard structural transformation techniques, where each concept occurring under a role restriction 9r:C or 8r:C is replaced by a new de ner D, for which we add a new axiom D v C. The resulting ontology can be brought into clausal form by applying standard conjunctive normal form transformations. As a result, the TBox of the input ontology is represented by a set of TBox clauses, and the ABox of the input ontology is represented by a set of role assertions, ABox clauses as well as TBox clauses, which give meaning to the introduced de ner symbols. The transformation can be done in polynomial time. Moreover, most ontologies are of a form that allows for a transformation in nearly linear time.
Example 1 (Normal form). The ontology O = fA v 8r:B; (C t 8r:(A t :B))(a); r(a; b)g is not in clausal form. The ontology N = f:A t 8r:D1, :D1 t B, C(a) _ (8r:D2)(a), :D2 t A t :B, r(a; b)g, where D1; D2 2 Nd, is in clausal form. N is equi-satis able with O, and is therefore the clausal representation of O. Literals of the form :D or :D(a), D 2 Nd are called negative de ner literals. An important invariant of the described transformation, which our calculus preserves, is that every TBox clause contains at most one negative de ner literal and that ABox clauses do not contain any negative de ner literals. This invariant ensures that we can always undo the structural transformation to eliminate introduced de ner symbols, to get back to the original signature of the ontology.
As shown in [
Role Assertion Instantiation:
C1 _ (8r:D)(a)
r(a; b) C1 _ D(b)
C1 t 8r:D
r(a; b) C1(a) _ D(b) provided C1 [ C2 does not contain a negative de ner literal.
ABox Existential Role Restriction Elimination:
C _ (9r:D)(a)
:D
C
to standard resolution calculi is that new de ner symbols are introduced
dynamically during the process. If the role propagation rule is applied, and there is a
de ner D12 for which N j= D12 v D1 u D2 holds, where N is our current set
of clauses, D12 is used in the conclusion. If such a de ner does not exist, D12 is
introduced as a new de ner and the clauses :D12 t D1 and :D12 t D2 are added
to the current clause set. This technique is key for termination of the calculus,
since only a nite number of de ner symbols is introduced [
If the ontology is consistent, ABox assertions have no in uence on entailed concept inclusions. This means the TBox of the uniform interpolant can be computed using the TBox rules. In order to compute the ABox of the uniform interpolant, we need the ABox rules shown in Figure 2. De ne A = :A and :A = A, and for any TBox clause C = L1 t : : : t Ln, let C(a) denote L1(a) _ : : : _ Ln(a). The ABox resolution, role propagation and existential role restriction elimination rules are adaptions of the corresponding TBox rules. The role assertion instantiation rules make use of role assertions to propagate universal role restrictions. While the conclusion of every ABox rule is an ABox clause, the ABox role propagation rules may introduce new de ners, and thus lead to additional TBox clauses in the current clause set.
Example 2 (ABox rules). Continuing on the clause set from the last example, we can apply ABox role propagation on :A t 8r:D1 and C(a) _ (8r:D2)(a), which results in the clause :A(a) _ C(a) _ (8r:D12)(a), where D12 is a new de ner that is introduced with the two clauses :D12 t D1 and :D12 t D2. Applying role assertion instantiation on the new derived clause and r(a; b) results in :A(a) _ C(a) _ D12(b).
Since the number of introduced de ners is bounded and clauses are represented as sets, it can be veri ed that the saturation of any nite set of clauses by the rules in Figure 1 and 2 is always nite. The calculus is also sound and refutationally complete, as the following theorem shows.
Theorem 1. The TBox and ABox rules form a sound and refutationally complete calculus and provide a decision procedure for satis ability of ALC-ontologies with non-empty TBoxes and ABoxes.
The calculus is used in the same way for forgetting concept and role symbols as
in [
When forgetting a role symbol r, the role assertion instantiation rule is
applied for all role assertions with this r. Then the role propagation rules on r are
used to derive all clauses of the form C t 9r:D and C _ (9r:D)(a), where D is
an unsatis able de ner. These existential restrictions are eliminated using the
existential role restriction elimination rules. In order to decide whether a de ner
is unsatis able, we can either use our own calculus or an external reasoner. (For
a rule-based representation of this procedure, see [
If our initial set of clauses is N, we denote the result by N x, where x is the symbol we want to forget. N x is the clausal representation of the result of forgetting x. In order to compute a uniform interpolant for a given signature , we iteratively forget every symbol x 62 using this method.
Theorem 2. Let N be any set of TBox and ABox clauses and x any concept or role symbol. Then, N x j= i N j= , for any ALC-axiom or ALC-assertion with x 62 sig( ). 4
In this section we describe how the introduced de ner symbols are eliminated, and how the result can be represented in an ontology without disjunctive concept assertions.
For eliminating de ners, the same technique as in [
O [ fD v Cg
O[D7!C] De ner Puri cation:
O
O[D7!>] Cyclic De ner Elimination:
O [ fD v C[D]g
O[D7! X:C[X]]
provided D 62 sig(C)
provided D occurs only positively in O
provided D 2 sig(C[D])
clauses that contain literals of the form D(a) are removed. As shown in the
long version of this paper [
Theorem 3. Let O be an ALC-ontology and sig(O). Let O be the result of forgetting all symbols in sig(O) n from the clausal representation of O, and eliminating all introduced de ners. Then, O is an ALC or ALC -ontology with possibly disjunctive ABox, and O is a uniform interpolant of O for .
The cyclic de ner elimination rule introduces xpoint operators to the
ontology. It is in general not always possible to nd a nite uniform interpolant
without xpoint operators. An alternative approach is to allow additional
symbols in the result, and simply not apply the cyclic de ner elimination rule. By
keeping the cyclic de ner symbols as \helper concepts" in the ontology, we
obtain an ontology that is not completely in the desired signature, but does not
use xpoint operators and preserves all entailments we are interested in. A third
alternative is to approximate the xpoint expressions in ALC as described in [
Using the role assertion instantiation rules, clauses with more than one individual can be derived, which will be represented as disjunctive concept assertions in the uniform interpolant. In general, there is no way to represent disjunctive concept assertions as classical concept assertions in ALC if the respective individuals are connected by role assertions, as the following lemma shows. Lemma 1. There are ALC-ontologies with disjunctive ABoxes that cannot be approximated by a nite ALC -ontology with a classical ABox in such a way that all entailments of the form C(a) or C v D are preserved, where C and D are ALC-concepts. This even holds if the ontology contains no cyclic role assertions. A consequence is that uniform interpolants of ALC-ontologies in general cannot be represented by ALC or ALC -ontologies with classical ABoxes. Theorem 4. There are ALC-ontologies O and signatures , such that there is no uniform interpolant of O for that is a nite ALC -ontology without disjunctive concept assertions.
A solution is to use nominals. If the individuals occurring in a disjunctive concept assertions are connected via role assertions, the assertion can be transformed using the following rule.
C _ C1(a) _ C2(b) r1(a; a1) r2(a1; a2) : : :
rn+1(an; b) C _ (C1 t 9r1: : : : 9rn+1:(fbg u C2))(a) (1) If r(a; b) 2 O, the concept 9r:fbg is already satis ed by a. The concept assertion (9r:(fbg u C2)(a) states additionally that the individual b also satis es C2. Therefore, concept assertions for b can be encoded inside concept assertions for a, if there is some path along the role assertions from a to b.
If there is no chain of role assertions between two individuals a and b, we cannot represent any information about b in a concept assertion of the form C(a). This happens when the connecting role symbols have been removed from the signature. However, it is possible to saturate clauses with unconnected individuals until these clauses are not needed anymore to preserve entailments of the form C(a). For example, if the uniform interpolant contains A(a) and :A(a) _ B(b), we can also represent it by the classical ABox A = fA(a); B(b)g. To make this approach practical, we use ordered resolution.
Let be any ordering between concept symbols and roles, and extend it to a total ordering l between TBox literals such that 8r:D 9r:D A :A for all r 2 Nr, D 2 Nd and A 2 Nc. Given an ABox clause C, a literal L(a) 2 C is maximal if for all literals of the form L0(a) 2 C we have L0 l L. Observe that if an ABox clause contains more than one individual name, it has more than one maximal literal.
We further keep a set Md of marked de ner symbols, which tells us which additional clauses we have to saturate. At the beginning, this set is empty. A clause is selected if it contains a pair of individuals that are not connected by a chain of role assertions, or a literal of the form :D with D 2 Md.
Given a set of clauses N, the set Nc is computed by saturating N using the TBox and ABox rules of Figures 1 and 2, with the following side conditions. { At least one clause in the premise of the rule must be selected. { Each rule is only applied on the maximal literals of the clauses. { If a maximal literal of selected clause is of the form 9r:D or (9r:D)(a), add D to Md.
The set Nc is saturated using Rule (1), and all concept assertions containing more than one individual are removed. We denote the result by NO. Since Rule (1) produces concept assertions that are not clauses, but ALCO-assertions, NO is not a clause set, but an ALCO-ontology.
Theorem 5. Let N be any set of clauses. Then, NO is an ALC or ALCOontology with classical ABox, and we have NO j= i N j= , where is of the form C v D, C(a) or r(a; b), and C and D are ALC-concepts.
Using this technique, uniform interpolants with disjunctions in the ABox can be transformed to ALCO or ALCO -ontologies with classical ABox. 5
In order to investigate how our method performs in practice, we implemented it
in Scala1 using the OWL-API,2 with some of the optimisations described in [
The evaluation was based on three ontologies. Family3 is the family ontology of Robert Stevens. It has a relatively complex TBox and its ABox consists only of role assertions. Semintec4 is an ontology about bank transactions, and has a simpler TBox but also a much larger ABox. The University Ontology Benchmark Generator (UOBM)5 comes with a tool that allows to generate ABoxes, and has a more complex TBox than Semintec. For our evaluation we generated an ontology for one university. All ontologies have been reduced to ALC by removing all axioms which are not in ALC, where we replaced domain and range restrictions, as well as number restrictions of the form 1r:C and 0r:C by equivalent expressions in ALC. We then generated 350 random signatures for each ontology, where each symbol was assigned a probability of 25% to be forgotten, and we computed uniform interpolants with and without disjunctive assertions. The uniform interpolants were represented in ALC and ALCO respectively using helper concepts, so that they could in theory be exported to OWL. The timeout for each experimental run was set to 60 minutes. 1 http://www.scala-lang.org 2 http://owlapi.sourceforge.net 3 http://www.cs.man.ac.uk/~stevensr 4 http://www.cs.put.poznan.pl/alawrynowicz/semintec.htm 5 http://www.cs.ox.ac.uk/isg/tools/UOBMGenerator
The results for computing uniform interpolants with disjunctive ABoxes are shown in Figure 4 and for computing uniform interpolants with classical ABoxes in Figure 5. The table shows the number of assertions in the ABox, the average size of an assertion of the respective ontology, the percentage of timeouts, the average duration, the average sizes of the output and the percentage of uniform interpolants that contained disjunctive assertions and nominals respectively.
Eliminating disjunctive assertions mostly took longer than forgetting the symbols. But as a result, only in a few cases nominals were necessary in the uniform interpolant, so that the uniform interpolants could in most cases be represented as ALC-ontologies. Also, the uniform interpolants with classical ABox had similar sizes to the respective input ontologies, except for the Semintec ontology. If nominals were used, the respective assertions were usually very complex. The timeouts were mainly caused by a small number of symbols. For example, forgetting the concept Person from the Family ontology always lead to a timeout, which caused 25% of the timeouts for this ontology.
We did not evaluate our method on ontologies with larger ABoxes, and there are probably some optimisations possible for large ABoxes that will improve the performance. However, in most realistic cases it is likely that, if the TBox is xed, the duration and the size of uniform interpolants are linear in the size of the ABox, since individuals are usually not overly connected and the reasoner can therefore process them in small independent groups for each symbol. 6
A lot of recent work covers uniform interpolation of TBoxes in description logics
of varying expressivity, including DL-Lite [22], E L [
The rst approach to compute uniform uniform interpolants of ALC-TBoxes
is based on a representation of the input ontology in disjunctive normal form,
from which incrementally a uniform interpolant is approximated [
Uniform interpolation of ALC-TBoxes is theoretically analysed in [
The early approaches for uniform interpolation in ALC required the
inputontology to be either directly or e ectively transformed into disjunctive normal
form, which is an unusual representation for ontologies. They also derive
consequences in an unrestricted way, which makes them unpractical for larger
ontologies. Practical uniform interpolation requires a more goal-oriented approach,
which is followed in [
Uniform interpolation involving ABoxes was rst investigated for the lightweight description logic DL-Lite [22]. Ontologies with ABoxes were also considered by the rst approach for uniform interpolation in ALC [21]. But this approach only works if the ABox is of a speci c form, since the result is always represented in ALC. 7
We presented a method for uniform interpolation of ALC-ontologies with ABoxes. In general, it is not always possible to represent these uniform interpolants in ALC or using xpoints. A solution is to either represent uniform interpolants in ALCO or to allow disjunctions in the ABox. Our evaluation suggests however, that these cases do not occur often in practice, and that uniform interpolants of ALC-ontologies with large ABoxes can be practically computed in most cases. We are currently working on extending the presented approach to more expressive description logics, for example, with number restrictions or inverse roles.
In this work we focused on preserving entailments that are expressible in ALC. Since the output of our method is represented in ALCO , it might be interesting to preserve ALCO-entailments as well. There are some entailments of this sort that our algorithm does not respect. For example, from the two ABox clauses A(a) _ :B(a) and B(b) one can deduce (A t :fbg)(a). Another restriction is our uniform interpolants only preserve entailments of the form C v D, C(a) and r(a; b). It would be interesting to investigate whether preserving further entailments, such as conjunctive queries, is possible.
Our method can only be used for forgetting concept and role symbols. An open question is how forgetting individuals can be performed. This would extend the possibilities of the approach for applications such as information hiding. 21. Wang, Z., Wang, K., Topor, R., Zhang, X.: Tableau-based forgetting in ALC ontologies. In: Proc. ECAI '10. pp. 47{52. IOS Press (2010) 22. Wang, Z., Wang, K., Topor, R.W., Pan, J.Z.: Forgetting for knowledge bases in DL-Lite. Ann. Math. Artif. Intell. 58(1{2), 117{151 (2010)