Towards Practical Uniform Interpolation and Forgetting for ALC TBoxes

Abstract

We develop a clausal resolution-based approach for computing uniform interpolants of TBoxes formulated in the description logic ALC when such uniform interpolants exist. We also present an experimental evaluation of our approach and its applications to concept forgetting, ontology obfuscation and logical difference on real-life ALC ontologies. Our results indicate that in many practical cases a uniform interpolant exists and can be computed with the presented algorithm.

Introduction

Ontologies or TBoxes expressed in Description Logics (DL) provide a common vocabulary for a domain of interest together with a description of the meaning of the terms built from the vocabulary and of the relationships between them. Modern applications of ontologies, especially in the biological, medical, or healthcare domain, often demand large and complex ontologies; for example, the National Cancer Institute ontology (NCI) consists of more than 60 000 term definitions. For developing, maintaining, and deploying such large-scale ontologies it can be advantageous for ontology engineers to concentrate on specific parts of an ontology and ignore or forget the rest, for example, in the following scenarios. Exhibiting hidden relations: in addition to the explicitly stated relations between terms, additional relations can also be derived from ontologies with the help of reasoners. Such inferred relations are often harder to understand or debug. By forgetting everything but a handful of terms of interest, it then becomes possible to exhibit inferred relations that are hidden initially, which can simplify the understanding of the ontology structure. Ontology obfuscation: in software engineering, obfuscation [ 4 ] transforms a given program into a functionally equivalent one that is more difficult to read and understand for humans for the purpose of preventing reverse engineering. Forgetting can provide a similar function in the context of ontology engineering. Terms are often defined with the help of auxiliary terms which help to give structure to TBox inclusions but such a structure might be considered proprietary knowledge that should not be exposed, or it could simply be of little interest for ontology users. By forgetting

This research was supported by EPSRC grant EP/E065279/1. these intermediate auxiliary terms, we obtain an ontology that is functionally equivalent, yet harder to read, understand, and modify by humans. Logical difference: when modifying an ontology, an ontology engineer usually wants to ensure that her changes do not interfere with the meaning of the terms outside the fragment under consideration. Such a correctness guarantee can be achieved by checking the equivalence of the ontologies resulting from forgetting the terms under consideration before and after the changes occurred. Further applications of forgetting can be found in [ 11, 12 ].

Ignoring parts of an ontology can be formalised with the help of predicate forgetting and its dual uniform interpolation, which have both been extensively studied in the AI and DL literature [ 3,6,8,11,13,16–18 ]. However, to the best of our knowledge, previous research in this area in the setting of DL mainly concentrates on theoretical foundations of forgetting and, except for practical work on lightweight description logics [ 11 ], we are not aware of any attempts to compute uniform interpolants for real-life ontologies in practice. This could be partly explained by the high computational complexity of this task and by the fact that uniform interpolants do not always exist.

In this paper we develop an algorithm based on clausal resolution for computing uniform interpolants of TBoxes formulated in the description logic ALC which can preserve all the consequences that do not make use of some given concept names. We also present an experimental evaluation of our approach which demonstrates that in many practical cases uniform interpolants exist and that they can be computed with our algorithm. All missing proofs can be found in the full version of this paper, which is available from http://lat.inf.tu-dresden.de/˜michel/publications/. 2

Preliminaries

We start with introducing the description logic ALC. Let NC and NR be countably infinite and mutually disjoint sets of concept names and role names. ALC-concepts are built according to the following syntax rule

C ::=

A j > j :C j 9r:C j

C u D; where A 2 NC and r 2 NR. As usual, other ALC concept constructors are introduced as abbreviations: ? stands for :>, C t D stands for :(:C u :D) and 8r:C stands for :9r::C. An ALC-TBox T is a finite set of ALC-inclusions of the form C v D, where C and D are ALC-concepts. A concept equation C D is an abbreviation for the two inclusions C v D and D v C. An ALC-TBox is acyclic if all its inclusions are of the form A v C and A C, where A 2 NC and C is an ALC-concept, such that no concept name occurs more than once on the left-hand side and T contains no cycle in its definitions, that is, it does not contain inclusions A1 ./ C1,. . . , Ak ./ Ck, where ./ 2 fv; g, such that Ai+1 occurs in Ci, for i = 1; : : : ; k 1 and Ak = A1.

A signature is a finite subset of NC [NR. The signature of a concept C, denoted by sig(C), is the set of concept and role names that occur in C. If sig(C) , we call C a -concept. We assume that the two previous definitions also apply to concept inclusions/equations C ./ D with ./ 2 fv; g and to TBoxes T . The size of a concept C is the length of the string that represents it, where concept names and role names are considered to be of length one. The size of an inclusion/equation C ./ D with ./ 2 fv; g is the sum of the sizes of C and D plus one. The size of a TBox T is the sum of the sizes of its inclusions.

The semantics of ALC is given by interpretations I = ( I ; I ), where the domain I is a non-empty set, and I is a function mapping each concept name A to a subset AI of I , each role name r to a binary relation rI I I . The extension CI of a concept C is defined by induction as follows: >I := (:C)I :=

I I n CI (9r:C)I := f d 2 I j 9e 2 CI : (d; e) 2 rI g (C u D)I := CI \ DI : Then I satisfies a concept inclusion C v D, in symbols I j= C v D, if CI DI .

We say that an interpretation I is a model of a TBox T if I j= C v D for all C v D 2 T . An ALC-inclusion C v D follows from (or is entailed by) a TBox T if every model of T is a model of C v D, in symbols T j= C v D. We use j= C v D to denote that C v D follows from the empty TBox. Finally, a TBox T 0 follows from (or is entailed by) a TBox T if every model of T is a model of T 0, in symbols T j= T 0.

We now introduce the main notion that we study in this paper.

Definition 1. Let T be an ALC-TBox and let sig(T ) be a signature. We say that an ALC-TBox T is a -uniform interpolant of the TBox T iff sig(T ) , T j= T , and for every ALC -concept inclusion C v D with T j= C v D it holds that T j= C v D.

Uniform interpolation can be seen as the dual notion of forgetting: a TBox T is the result of forgetting about a signature in a TBox T iff T is a uniform interpolant of T w.r.t. = sig(T ) n . As the following example shows, uniform interpolants of ALC-TBoxes do not always exist.

Example 2. Let T = fA v B; B v C u 9r:Bg and = fA; C; rg. Then there does not exist a -uniform interpolant of T as (in particular) the infinite number of consequences of the form A v 9r:C, A v 9r:9r:C; : : : cannot be captured by an ALC-TBox T 0 with sig(T 0) . On the other hand, for T 0 = fA v B; B v C u 9r:B; D Bg and 0 = fA; C; D; rg, a 0-uniform interpolant of T 0 is fA v D; D v C u 9r:Dg.

A 2-EXPTIME-complete bound on the complexity for deciding the existence of a -uniform interpolant in ALC and a worst-case triple-exponential procedure for computing a -uniform interpolant if it exists, have been given in [ 13 ]. The proof of the upper bound proceeds by ‘internalisation’ of the TBox: if a -uniform interpolant exists, then there exists a concept CT of size double exponential in the size of T having the property that for any -inclusion C v D it holds that T j= C v D iff j= C u CT v D. Then the authors compute C0, a -concept uniform interpolant [ 3 ] of CT , and show that > v C0 is a -uniform interpolant of T . 3

Computing Uniform Interpolants by ALC-Resolution

The aim of our work is to investigate a practical approach for computing uniform interpolants when they exist. Note that the procedure given in [ 13 ] is inherently inefficient as it requires one to explicitly construct the double-exponential size internalisation CT of a given TBox T .

Our approach is to introduce a resolution-like calculus for ALC that derives consequences of a TBox T such that a concept inclusion C v D is entailed by T iff a contradiction can be derived from T and C u :D. Similarly to [ 8 ], we then show that any derivation can be restructured in such a way that inferences on selected concept names always precede inferences on other concept names. Then, if the signature is such that sig(T ) n only contains concept names, we generate a set of -consequences T 0 of T by applying the inference rules in a forward chaining manner such that for an arbitrary -inclusion C v D a contradiction can be derived from T and C u :D iff a contradiction can be derived from T 0 and C u :D. Thus, if the forward-chaining process terminates, T 0 is a -uniform-interpolant for T .

ALC-Resolution. ALC-resolution operates on ALC formulae in conjunctive normal form defined according to the following grammar (this is similar to [ 8 ]): Literal ::= A j :A j 8r:Clause j 9r:CNF Clause ::= Literal j Clause t Clause j ?

CNF ::= > j Clause j Clause u CNF To simplify the presentation, we assume that clauses are sets of literals and that CNF expressions are sets of clauses. Then ? corresponds to the empty clause and > to the empty set of clauses. In the following, the calligraphic letters C; D; E symbolise clauses and F ; G represent sets of clauses. Similarly to first-order formulae, every ALC concept can be transformed into an equivalent set of ALC clauses. The depth of a clause C, Depth(C), is defined to be the maximal nesting depth of the quantifiers contained in C.

We additionally assume that every clause is assigned a type. Clauses obtained from the clausification of TBox inclusions are of the type universal, and clauses resulting from the clausification of inclusions to be tested for entailment by the TBox are of the type initial. The type of a derived clause is determined by the types of the clauses from which it is derived and by the derivation rule that is used.

Example 3. The clausification of T from Example 2 produces three universal clauses: :A t B; :B t C; :B t 9r:B.

We now introduce the two resolution calculi T and Tu. The former calculus assumes the TBox to be empty, whereas the latter takes TBox inclusions into account. Thus, T derives the empty clause from the set of initial clauses stemming from the clausification of an inclusion C v D iff j= C v D; and Tu derives the empty clause from the universal clauses stemming from the clausification of a TBox T and the initial clauses stemming from the clausification of an inclusion C v D iff T j= C v D.

The calculus T is defined with the help of the relation ) given in Fig. 1. For every 2 NC [ f?g, the relation ) associates with a set of clauses N a new clause C which can be ‘derived’ from the set N by ‘resolving’ on . T now consists of the following two inference rules.

C (if C ) E )

E where C; D, and E are initial clauses.

C

E

D (if C; D )

E ); (rule ?) (rule A) (rule 89) (rule 88) C10 t 8r:C1; C20 t 8r:C2 =) C0 t 9r:(C1; F ) =)

C0 t 9r:(C1; F ; C2)

C10 t C20 t 9r:(C2; F ; C3)

if C1; C2 =) C3 C10 t C20 t 8r:C3

if C1; C2 =) C3 C0 t 9r:(C1; C2; F ) =) C0 t 8r:C1 =)

C0 t 8r:C2

if C1 =) C0 t 9r:(C1; C2; F ; C3) if C1; C2 =) if C1 =)

C2 C3 C2

The calculus Tu operates initial and universal clauses and also consists of two rules:

C0

EC (if C ) E ) E 0 D (if C0; D )u E 0); where C, C0, D are initial or universal clauses, and C0; D )u E 0 holds iff either C0; D ) E 0, or D is a universal clause and there exist role names r1; : : : ; rn 2 NR (n 1) such that C0; 8r1: : : : 8rn:D ) E 0. (Intuitively, the calculus Tu allows for inferences with universal clauses at arbitrary nesting levels of quantifiers, which the calculus T does not.) Then E is a universal clause if C is a universal clause, and an initial clause otherwise. Similarly, E 0 is a universal clause if both C0 and D are universal clauses, and an initial clause otherwise.

Example 4. For the universal clauses from Example 3, we have for instance, :A t B; :B t 9r:B )B :A t 9r:B by (rule A): So, the universal clause :A t 9r:B is derivable by Tu from :A t B and :B t 9r:B. As :B t C is a universal clause and

:B t 9r:B; 8r::B t C )B :B t 9r:(B; C) by (rule 89); the universal clause :B t 9r:(B; C) is derivable by Tu from :B t 9r:B and :B t C. By applying the inference rules to old and newly generated clauses, one can conclude that the universal clauses :A t 9r:(B; C) and :A t 9r:(B; 9r:B) are also derivable by Tu from N = f:A t B; :B t C; :B t 9r:Bg.

For x 2 fT; Tug, a x-derivation (tree) built from a set of clauses N is a finite binary tree where each leaf is labelled with a clause from N and each non-leaf node n is labelled with a clause C such that C results from an x-inference on the parent(s) of n in . We say that is a derivation of a clause C if the root of is labelled with C. A derivation of the empty clause is called a refutation. Every path n1; : : : ; nm of nodes in where n1 is a leaf node and nm is the root node induces an inference path 2; : : : ; m where i 2 NC [ f?g (2 i m) denotes the concept name, or ?, which has been resolved upon to obtain the clause that is the label of the node ni. For a signature NC and a strict total order , a derivation is a (x; ; )derivation if for every inference path 1; : : : ; n of (with i 2 NC [ f?g for every 1 i n) there exists 0 k n such that f 1; : : : ; kg , j j+1 or j = j+1 for every 1 j < k, and j 62 for every k < j n.

The calculus T is a direct adaption of the calculus for the modal logic K introduced in [ 7 ] to ALC, and so j= > v C iff the empty clause can be derived from the clausification of :C. However, as we show in the full version of the paper, the proof given in [ 7 ] of the fact that any derivation in T can be reordered so that inferences on concept names from always precede inferences on other concept names, or ?, appears to have some gaps. We prove the following theorem which extends the results stated in [ 8 ]. Theorem 5 (T-Completeness). Let NC, let be a strict total order on and let C be an ALC concept. Then it holds that j= C v D iff there exists a (T; ; )-derivation of the empty clause from the initial clauses Cls(C u :D). To prove completeness for Tu, we observe the following link between derivations in T and Tu. Let N be a set of clauses and let Univ0(N ) = N ; and Univ(N ) = Si 0 Univi(N ).

Univi+1(N ) = Univi(N ) [ r2NR\sig(N ) [ f 8r:D j D 2 Univi(N ) g Theorem 6. Let M be a set of initial clauses and let N be a set of universal clauses. Additionally, let be a (T; ; )-refutation from M [ Univ(N ) such that there exists n 2 N with Depth(C) n for every C 2 Clauses( ). Then there exists a (Tu; ; )derivation u of the empty clause from M [ N such that Depth(C) n for every C 2 Clauses( u).

We then use Theorem 5 and the fact that every ALC-TBox can be internalised. Notice that the actual TBox internalisation CT does not have to be computed as it is only used for the proof of completeness.

Corollary 7 (Tu-Completeness). Let T be an ALC-TBox, let NC, let

be a strict total order on and let C be an ALC concept. Then it holds that T j= C v D iff there exists a (Tu; ; )-derivation of the empty clause from the universal clauses Cls(T ) and the initial clauses Cls(C u :D).

Computing Uniform Interpolants. The procedure UNIFORMINTERPOLANT depicted in Algorithm 1 takes as input an ALC-TBox T , a signature sig(T ) such that \ NR = sig(T ) \ NR and a strict total order over = sig(T ) n . Following the outline of [ 8 ], after the clausification of T , the procedure iterates over the concept names contained in in descending order according to the relation . In each iteration all possible Tu-inferences on the current concept name A 2 from the clause set N obtained in the previous iteration are computed. Finally, after iterating over all the concept names from = sig(T ) n , the operator ‘Supp’ is applied on the resulting clauses, which replaces all occurrences of concept names in clauses with > and then simplifies the resulting CNF.

Algorithm 1 1: procedure UNIFORMINTERPOLANT(T , , ) 2: := sig(T ) n 3: N := Cls(T ) 4: while 6= ; do 5: A := max ( ) 6: N := ResT1u;fAg(N ) 7: := n fAg 8: end while 9: return F (T ) = Supp(sig(T ) n ; N ) 10: end procedure Example 8. For the clauses derived in Example 4, Supp(fBg; :A t C) = A t C, Supp(fBg; :A t 9r:B) = :A t 9r:>, Supp(fBg; :A t 9r:(B; C)) = :A t 9r:C.

One can show that if Algorithm 1 terminates, for all ALC -concepts C; D such that there exists a (Tu; ; )-refutation u from the universal clauses Cls(T ) and the initial clauses Cls(C u :D) it holds that F (T ) j= C v D. Thus, it follows from Corollary 7 that if Algorithm 1 terminates, it computes a -uniform interpolant of T . However, Algorithm 1 does not terminate if a uniform interpolant does not exist. For example, when applied to T from Example 2, Algorithm 1 can generate, among others, the infinite sequence of universal clauses :A t 9r:C, :A t 9r:(C; 9r:C); : : : and so it does not terminate. Moreover, as T from Example 2 is a subset of T 0, and so Cls(T ) Cls(T 0), Algorithm 1 will derive, among others, the same clauses when it is applied on T 0. Thus, in some cases Algorithm 1 does not terminate even though a uniform interpolant exists.

To guarantee termination on all inputs, we focus on the notion of depth-bounded uniform interpolation (related to the notion of ‘bounded forgetting’ [19]). Let T be an ALC-TBox and let sig(T ) be a signature. We say that an ALC-TBox T is a depth n-bounded uniform interpolant of the TBox T w.r.t. iff sig(T ) , T j= T , and for every ALC -concept inclusion C v D with T j= C v D and maxfDepth(C); Depth(D)g n it holds that T j= C v D. Let F ;m(T ) be the outcome of Algorithm 1 where in Step 6 only clauses up to depth m are generated. The following example shows that it might be necessary to consider intermediate clauses of a depth m > n in order to preserve all the -consequences of depth n entailed by T . Example 9. Let T = f:At9r:C; :C t9s:>; B t8s:?g, = fA; B; r; sg, = fCg and = ;. Then every (Tu; ; )-refutation from the universal clauses Cls(T ) and the initial clauses fA; 8r::Bg derives the clause :A t 9r:(C; 9s:>).

We establish, however, that by choosing the maximal depth of derived clauses appropriately, the procedure depicted in Algorithm 1 computes uniform interpolants that preserve consequences up to a specified depth n.

Theorem 10. Let T be an ALC-TBox, sig(T ) a signature such that \ NR = sig(T ) \ NR, and let n 0. Set m = n + 2jsub(Cls(T ))j+1 + maxf Depth(C) j C 2 Cls(T ) g. Then it holds that F ;m(T ) is a depth n-bounded uniform interpolant of the TBox T w.r.t. .

We can combine this result with the bound on the size of uniform interpolants in [ 13 ]: for any ALC-TBox T and signature (with \ NR = sig(T ) \ NR), if a -uniform interpolant of T exists, there exists m, which can be computed based on the bound in Theorem 10 and the results of [ 13 ], such that F ;m(T ) is a -uniform interpolant of T .

The bound in Theorem 10 can be significantly improved if the TBox is acyclic. For an acyclic ALC-TBox T we define ExpansionDepth(T ) = maxf Depth(A[T ]) j A 2 sig(T ) g, where A[T ] denotes the concept obtained by exhaustively replacing every concept B with CB if B v CB 2 T or B CB 2 T .

Theorem 11. Let T be an acyclic ALC TBox, sig(T ) a signature such that \ NR = sig(T ) \ NR, and let n 0. Set m = ExpansionDepth(T ) + n. Then it holds that F ;m(T ) is a uniform interpolant limited to consequence depth n of the TBox T w.r.t. .

Note that in the description logic E L (i.e. the fragment of ALC that does not allow ?, negation, disjunction, or universal quantification) the acyclicity of a TBox guarantees the existence of uniform interpolants [ 11 ] for any signature . Interestingly, this is not so in the case of ALC. Moreover, as the following example shows, there exists an acyclic E L-TBox T and a signature for which no ALC -uniform interpolant exists. Example 12. Consider = fA; A0; A1; A2; E; rg and T = fA v 9r:B, A0 v 9r:(A1 u B), E A1 u B u 9r:(A2 u B)g. Then for every n 0

n T j= A0 u l 8r: : : : 8r:(A u :E u (A1 t A2)) v 9r: : : : 9r: A1:

i=1 | {iz } | {nz } This infinite sequence of ALC consequences of T cannot be captured by any ALC TBox T 0, which can be proved formally using the criterion ( m) of Theorem 9 in [ 13 ]. 4

Case Study

We have implemented a prototype of an inference computation architecture using the calculus Tu and the inference relation ) in Java. It has turned out that our initial implementation of Algorithm 1 did not perform well in practice. This is in particular due to the fact that clauses can contain sets F of other clauses in existential literals 9r:F , which renders all the possible inferences on clauses from F ‘explicit’. For example, if we resolve the universal clause which just consists of the existential literal 9r:(A) with the universal clauses :A t B1; : : : ; :A t Bn on the concept name A, then not only the clauses 9r:(A; B1), 9r:(A; B2), 9r:(A; B3),. . . could be derived but all clauses of the form 9r:(A; G), where G is a subset of fB1; : : : ; Bng.

A common technique to reduce the number of inferences that have to be made is to use forward- and backward deletion of subsumed clauses [ 2 ]. However, it is known [ 1 ] that the subsumption lemma (stating that if a clause E results from an inference involving two clauses C and D, and if there exist clauses C0, D0 such that C0 subsumes C and D0 subsumes D, then either E is subsumed by one of C0, D0, or a clause E 0 can be derived from C0 and D0 such that E 0 subsumes E ) does not hold even in the modal logic K for the standard minimal subsumption relation s and ) . To be able to prove that one can safely discard subsumed clauses, we have modified the inference relation ) by introducing the following additional rule (rule 9f )

C1 t 8r:D; C2 t 9r:F =)9f C1 t C2 t 9r:(F ; D): We will denote the resulting inference relation by )f with 2 NC [ f?; 9f g. One can then prove that a variant of the subsumption lemma holds for the relations s and )f , which allows us to employ forward- and backward deletion of subsumed clauses in our implementation.

In order to further speed up computations, we first extract the locality-based >? -module [ 5, 14 ] for a given TBox T . The locality-based module entails the same inclusions as the TBox T but it is often considerably smaller in size. We also rely on ontologies to have structure: if a concept name occurs in several inclusions, it is likely that it occurs in the same syntactic pattern. Thus, 1. If the clause set contains some clauses C1 t D ; : : : ; Cm t D such that for every 1 i m we have sig(Ci) \ = ;, we rewrite them into X t D , where X C1 u : : : u Cm, perform forgetting on symbols and then replace X with its definition. 2. If the clause set contains a clause C t 9r:(F ; G1) t : : : t 9r:(F ; Gm) where sig(Gi) \ = ; for every 1 i m, we rewrite it into C t 9r:(F ; Y ), where Y G1 t : : : t Gm, perform forgetting on and then replace Y with its definition. Experimental setting. All experiments were conducted on PCs equipped with an Intel Core i5-2500K CPU running at 3.30GHz. 15 GiB of RAM were allocated to the Java VM and an execution timeout of 60 CPU minutes was imposed on each problem. We only considered ALC-fragments of ontologies, i.e. for a given ALC-ontology T we removed all the axioms which contain non-ALC concept (or role) constructors to obtain its ALC-fragment. We used Algorithm 1 to forget concept names one by one (i.e. for sig(T ) n = fA1; : : : ; Ang, Algorithm 1 was applied iteratively on A1; : : : ; An), and we did not impose a bound on the depth of clauses. After each run of Algorithm 1 we further simplified the resulting clause set N by removing clauses D for which there exists C 2 N with C s D. Thus, in all the experiments reported on in this section we computed true -uniform interpolants (i.e. not a depth-bounded variant). The correctness of our extensions to Algorithm 1 can be shown by model-theoretic arguments. Exhibiting Hidden Relations. We applied our uniform interpolation tool to compute uniform interpolants w.r.t. small signatures sig(T ) with sig(T ) \ NR = \ NR for a fragment of version 1.4 of the Drug Interaction Knowledge Base3 (DIKB) and for a fragment of version 08.10e of the National Cancer Institute Thesaurus4 (NCI) that are of expansion depth 3 (that is, we removed all the axioms from both ontologies that led to an expansion depth greater than 3). The resulting DIKB fragment is a small acyclic terminology that contains 120 concept names, 27 roles names, and 127 axioms. The NCI fragment is also an acyclic terminology with 53571 concept names, 78 role names and 62494 axioms (of which 2362 are of the form A C). For each considered sample size x and terminology T we generated 100 signatures by randomly choosing x concept names from sig(T ) and by adding all the role names from sig(T ) to . 3 Available from http://bioportal.bioontology.org/ontologies/1672 4 Available from http://evs.nci.nih.gov/ftp1/NCI_Thesaurus

Ontology j \ NCj DIKB v1.4 NCI v08.10e 5 10 15 50 100 150

Successful Computations 85 60 44 65 56 41

Average Nr of Axioms 7:482 14:033 25:114 21:369 41:089 63:146

Average Maximal

Axiom Size 19:176 24:933 26:568 30:538 62:839 104:756

The results that we obtained for the two ontologies are shown in Table 1. The third column gives the number of signatures for which a uniform interpolant could be computed within the given time limit, and the average number of axioms and the average of the maximal size of the axioms contained in each uniform interpolant are shown in the subsequent columns. Most uniform interpolants could be computed within 60 seconds. In a few cases, however, the computations took up to 3487 seconds.

One can see that the number of successful computations decreased with increasing size of \ NC, which seems to be due to the fact that the >? -modules then contain more symbols that lead to a large number of inferences. Most uniform interpolants that we have obtained are relatively small and contain a lot of expressions of the form 9r1 : : : 9rn:>. In some cases the process of forgetting certain intermediate concept names generated a few hundred clauses that were simplified or deleted in the remaining computation steps.

Ontology Obfuscation. As a proof of concept, we applied our uniform interpolation tool on (a fragment of) the Lipid Ontology5 (LiPrO) to forget 45 concept names which are intermediate concept names in the ontology’s induced concept hierarchy, i.e. those concept names group certain subconcepts together to give structure to the ontology. LiPrO is an acyclic terminology with 593 axioms, 574 concept names and one role name. The maximal size of an axiom is 50.

It then took 192 CPU seconds to compute the uniform interpolant, which contains 3415 axioms with a maximal size of 283. The uniform interpolant that we computed thus approximately contains 6 times more axioms than the original ontology and the maximal axiom size has increased by a factor of 6 as well. Notice that most of the original structure of the ontology has been destroyed while preserving all the consequences entailed by the retained concept names.

Logical Difference. We also used our implementation for the computation of the logical difference [ 9 ] between two versions of the NCI thesaurus on various signatures. The -logical difference between ALC-TBoxes T1 and T2 is the set Di (T1; T2) of all ALC-concept inclusions C v D such that sig(C v D) , T1 j= C v D, and T2 6j= C v D. Notice that if Di (T1; T2) is nonempty, it is infinite already.

It is easy to see that Di

(T1; T2) = ; if, and only if, T2 j= T1( ) where T1( ) is a -uniform interpolant of T1. Moreover, if T2 6j= T1( ), every inclusion C v D 2 T1( ) 5 Available from http://bioportal.bioontology.org/ontologies/1183 with T2 6j= C v D is said to be a witness of Di (T1; T2). In our experiments we used the reasoner FaCT++ v1.6.2 [ 15 ] to determine whether any axiom C v D 2 T1( ) is a witness of Di (T1; T2). To make the experiments more challenging for the reasoner, we focused on comparing (a fragment of) NCI v08.10e (as T1) with (a fragment of) NCI v.08.09d (as T2), both limited to an expansion depth of 3, on large signatures with \NR = sig(T )\NR. In that way the computed uniform interpolants remain rather large as well. For each sample size x 2 f50; 100; 150g we again generated 100 signatures by randomly choosing jsig(T )\NCj x concept names from sig(T ) and by including all the role names from sig(T ). The results that we obtained are now shown in Table 2. Note that these results are not directly comparable with the logical difference for the description logics of the E L family [ 9, 10 ] as illustrated by Example 12.

One can observe that as size of sig(T ) n increases, i.e. more symbols have to be forgotten from the >? -modules, the success rate dropped slightly. Overall, the average number of witnesses and the average maximal size of the witnesses remains comparable throughout the different sample sizes. Also, the axioms generated by the computation of the uniform interpolant did not pose a problem for FaCT++ as computing the logical difference for a given signature never took more than 20 seconds in our experiments. 5

Conclusion

In this paper we presented an approach based on clausal resolution for computing uniform interpolants of ALC-TBoxes T w.r.t. signatures sig(T ) that contain all the role names present in T . We proved that whenever the saturation process under ALCresolution terminates, the algorithm computes a uniform interpolant. To guarantee termination on all inputs, we introduced a depth-bounded version of our algorithm. We showed that by choosing an appropriate bound on the depth of clauses, one can axiomatise all -inclusions implied by the given TBox up to a specified depth. Combined with a known bound on the size of uniform interpolants, our depth-bounded procedure always computes a uniform interpolant if it exists.

In the second part of this paper we investigated how often our unrestricted resolutionbased algorithm terminates with a uniform interpolant by applying our prototype implementation on a number of case studies. Our findings suggest that despite a high computational complexity uniform interpolants can be computed in many practical cases. The computation procedure could further benefit from better redundancy elimination techniques, which, together with extending our approach to forgetting role names, constitutes future work. It would also be interesting to explore proof strategies for our resolution calculi that guarantee termination when uniform interpolants exist. 18. Wang, Z., Wang, K., Topor, R.W., Zhang, X.: Tableau-based forgetting in ALC ontologies.

In: Proceedings of the 19th European Conference on Artificial Intelligence (ECAI 2010).

Frontiers in Artificial Intelligence and Applications, vol. 215, pp. 47–52 (2010) 19. Zhou, Y., Zhang, Y.: Bounded forgetting. In: Proceedings of the Twenty-Fifth AAAI Conference on Artificial Intelligence (AAAI 2011). AAAI Press (2011)

References

1. Auffray , Y. , Enjalbert , P. , He´brard, J.J.: Strategies for modal resolution: Results and problems . Journal of Automated Reasoning 6 ( 1 ), 1 - 38 ( 1990 )

2. Bachmair , L. , Ganzinger , H.: Resolution theorem proving . In: Handbook of automated reasoning , vol. 1 , chap . 2, pp. 19 - 99 . Elsevier ( 2001 )

3. ten Cate, B. , Conradie , W. , Marx , M. , Venema , Y. : Definitorially complete description logics . In: Proceedings of the Tenth International Conference on Principles of Knowledge Representation and Reasoning (KR 2006 ). pp. 79 - 89 . AAAI Press ( 2006 )

4. Collberg , C.S. , Thomborson , C.D. , Low , D. : Manufacturing cheap, resilient, and stealthy opaque constructs . In: Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '98) . pp. 184 - 196 . ACM ( 1998 )

5. Cuenca Grau , B. , Horrocks , I. , Kazakov , Y. , Sattler , U. : Modular reuse of ontologies: theory and practice . Journal of Artificial Intelligence Research (JAIR) 31 , 273 - 318 ( 2008 )

6. Eiter , T. , Ianni , G. , Schindlauer , R. , Tompits , H. , Wang , K. : Forgetting in managing rules and ontologies . In: Proceedings of the 2006 IEEE / WIC / ACM International Conference on Web Intelligence (WI 2006 ). pp. 411 - 419 . IEEE Computer Society ( 2006 )

7. Enjalbert , P. , del Cerro , L.F. : Modal resolution in clausal form . Theoretical Computer Science 65 ( 1 ), 1 - 33 ( 1989 )

8. Herzig , A. , Mengin , J.: Uniform interpolation by resolution in modal logic . In: Proceedings of the 11th European Conference on Logics in Artificial Intelligence (JELIA 2008 ). Lecture Notes in Computer Science , vol. 5293 , pp. 219 - 231 . Springer ( 2008 )

9. Konev , B. , Walther , D. , Wolter , F. : The logical difference problem for description logic terminologies . In: Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR 2008). Lecture Notes in Computer Science , vol. 5195 , pp. 259 - 274 . Springer ( 2008 )

10. Konev , B. , Ludwig , M. , Walther , D. , Wolter , F. : The logical difference for the lightweight description logic E L . Journal of Artificial Intelligence Research (JAIR) 44 , 633 - 708 ( 2012 )

11. Konev , B. , Walther , D. , Wolter , F. : Forgetting and uniform interpolation in large-scale description logic terminologies . In: Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI 2009 ). pp. 830 - 835 ( 2009 )

12. Lutz , C. , Seylan , I. , Wolter , F. : An automata-theoretic approach to uniform interpolation and approximation in the description logic E L . In: Proceedings of the Thirteenth International Conference on Principles of Knowledge Representation and Reasoning (KR 2012 ). AAAI Press ( 2012 )

13. Lutz , C. , Wolter , F. : Foundations for uniform interpolation and forgetting in expressive description logics . In: Walsh, T . (ed.) Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI 2011 ). pp. 989 - 995 ( 2011 )

14. Sattler , U. , Schneider , T. , Zakharyaschev , M. : Which kind of module should I extract? In: Proceedings of the 22nd International Workshop on Description Logics (DL 2009 ). CEUR Workshop Proceedings , vol. 477 . CEUR-WS.org ( 2009 )

15. Tsarkov , D. , Horrocks , I.: FaCT++ Description Logic reasoner: System description . In: Proceedings of the Third International Joint Conference on Automated Reasoning (IJCAR 2006). Lecture Notes in Computer Science , vol. 4130 , pp. 292 - 297 . Springer ( 2006 )

16. Wang , K. , Wang , Z. , Topor , R. , Pan , J.Z. , Antoniou , G.: Eliminating concepts and roles from ontologies in expressive descriptive logics . Computational Intelligence ( Accepted for publication) , DOI: 10 .1111/j.1467- 8640 . 2012 . 00442 .x

17. Wang , Z. , Wang , K. , Topor , R. , Pan , J.Z. : Forgetting Concepts in DL-Lite . In: Proceedings of the 5th European Semantic Web Conference (ESWC2008). Lecture Notes in Computer Science , vol. 5021 , pp. 245 - 257 . Springer ( 2008 )