We present a method for forgetting concept symbols in ontologies speci ed in the description logic ALCOI. The method is an adaptation and improvement of a second-order quanti er elimination method developed for modal logics and used for computing correspondence properties for modal axioms. It follows an approach exploiting a result of Ackermann adapted to description logics. Important features inherited from the modal approach are that the inference rules are guided by an ordering compatible with the elimination order of the concept symbols. This provides more control over the inference process and reduces non-determinism, and the size of the search space. The method is extended with a new case splitting inference rule, and several simpli cation rules. Compared to related forgetting and uniform interpolation methods for description logics, the method can handle inverse roles, nominals and ABoxes. Compared to the modal approach on which it is based, it is more e cient in time and has higher success rates. The method has been implemented in Java using the OWL API. Preliminary experimental results show that the order in which the concept symbols are eliminated signi cantly a ects the success rate and e ciency.
Ontology-based technologies provide novel ways of building knowledge
processing systems and play an important role in many di erent areas, both in research
projects but also in industry applications. Big ontologies contain however large
numbers of symbols and knowledge modelled in them is rich and inevitably
heterogeneous. Thus there are situations, where it is useful to be able to restrict
the ontology to a subset of the signature and forget those symbols which do not
belong to the subset, for example, when an ontology needs to be analysed by
an ontology engineer to gain an understanding of the information represented
in it. Another example is a scenario where ontologies are distributed at separate
remote sites and information is exchanged via agents. Since the vocabularies
known to the agents at the di erent sites will vary, communication between the
agents needs to be limited to using the common language to avoid ambiguity
and confusion caused by the inconsistency of the vocabularies being used. At
this point, it would be bene cial if the signature symbols in one ontology that
are not known to the other agents can be eliminated without losing information
required for the communication. In other words, signature symbols belonging
to only one of the ontologies are forgotten, and communication is restricted to
information expressed in the shared language of the agents' ontologies. Another
use of forgetting is restricting the vocabulary of an ontology to more general
concept symbols, and forgetting those that are more speci c, to create a
summary of the ontology [
The contribution of this paper is the presentation of a method for forgetting
concept symbols in ontologies speci ed in the description logic ALCOI. ALCOI
extends the description logic ALC with nominals and inverse roles. Forgetting
concept symbols for ALCOI is a topic where no method is available yet, but a
number of related methods exist. Forgetting can be viewed as the problem dual
to uniform interpolation. A lot of recent work has been focussed on uniform
interpolation of mainly TBoxes represented in several description logics, ranging
from ones with more limited expressivity, such as DL-Lite [
Forgetting can however also be viewed as a second-order quanti cation
problem, which is the view we take in this paper. In second-order quanti er
elimination, the aim is to eliminate existentially quanti ed predicate symbols in order
to translate second-order formulae into equivalent formulae in rst-order logic [
Our method is adapted from a method, called Msqel, designed for modal
logic to compute rst-order frame correspondence properties for modal axioms
and rules [
De nition of ALCOI and Other Basic De nitions Let NC and NR be the set of atomic concepts and the set of atomic roles, respectively, and let NO be the set of nominals. ALCOI-concepts have one of these forms:
a j ? j > j A j :C j C t D j C u D j 9R:C j 9R :C j 8R:C j 8R :C, where a 2 NO, A 2 NC , R 2 NR, and C and D are arbitrary ALCOI-concepts. R denotes the inverse of the role R. By de nition, R is expressively the same as R.
An ontology usually consists of two parts, namely a TBox and an ABox. A TBox contains a set of axioms of the form C v D or C D, where C and D are concepts. A concept de nition C D can be expressed by two general inclusion axioms C v D and D v C. In ALCOI, ABox axioms can be expressed as inclusions in the TBox: a concept assertion C(a) can be expressed as a v C, and a role assertion R(a; b) as a v 9R:b. In this paper, we treat the ABox axioms as inclusions, consequently in our considerations ALCOI-ontologies are assumed to contain TBox axioms only.
We de ne an interpretation I for ALCOI over the signature (NC , NR, NO) as the pair h I ;:I i, where I is a non-empty set that represents the interpretation domain, and :I is the interpretation function that assigns to every nominal a 2 NO a singleton set aI I ; to every concept symbol A 2 NC a subset AI of I ; and to every role symbol R 2 NR a subset RI of I I . We specify the semantics of ALCOI-concepts by extending the interpretation function to the following:
?I = ; (8R:C)I = fx 2 (9R:C)I = fx 2 (:C)I =
I nCI
(C t D)I = CI [ DI I j 8y:(x; y) 2 RI ! y 2 CI g
I j 9y:(x; y) 2 RI ^ y 2 CI g (R )I = f(y; x) 2
I
I j (x; y) 2 RI g
The semantics of the TBox-axioms is de ned as follows: an interpretation I satis es C v D i CI DI , and I satis es C D i CI DI . If O is a set of TBox axioms, I is a model of O i it satis es every axiom in O, denoted by I j= O.
In the rest of the paper, we also need the following de nitions. A clause is a disjunction of ALCOI-concepts. Let A be a concept symbol and let I and I0 be interpretations. We say I and I0 are A-equivalent, if I and I0 coincide but di er possibly in the valuation assigned to A. This means their domains coincide, i.e.,
I = I0 , and for each symbol s in the signature except for A, sI = sI0 . More generally, suppose = fA1; : : : ; Amg NC , I and I0 are -equivalent, if I and I0 are the same but di er possibly in the valuations assigned to the concept symbols in . 3
We are interested in forgetting concept symbols in axioms of an ontology O of TBox axioms. Let sig(O) denote the signature of O.
De nition 1. Let O and O0 be ALCOI-ontologies and let = fA1; : : : ; Amg be a set of concept symbols. O0 is the result of forgetting the symbols in from O, if sig(O0) sig(O)n
and for any interpretation I, I j= O i
I0 j= O0 for some interpretation I0 -equivalent to I.
The symbols in are the symbols to be forgotten. We refer to them as the non-base symbols and the symbols in sig(O)n as the base symbols. The result of forgetting a concept symbol A from O is the result of forgetting fAg from O.
The result of forgetting a symbol A from an ontology O can be represented
as 9X OXA in the extension of the language with existentially quanti ed concept
variables. OXA is our notation for substituting every occurrence of A is O by X.
In general, for the target language which extends the (source) language of the
logic under consideration with existential quanti cation of predicate symbols, the
result of forgetting always exists. The challenge of forgetting, as a computational
problem, is to nd an ontology O0 (without any occurrences of X) in the source
language (without second-order quanti cation) that is equivalent to 9X OXA ,
where O is expressed in the source language. Finding such an ontology O0 that
is equivalent to 9X OXA is an instance of the second-order quanti er elimination
problem. Forgetting a concept symbol A is thus the problem of eliminating the
existential quanti er 9X from 9X OXA . In the following, we slightly informally
say the aim is to eliminate the symbol A from O. For this we apply second-order
quanti er elimination techniques to the axioms of O in order to forget A (the
non-base symbol). In particular, we are going to exploit an adaptation of a result
of Ackermann [
Theorem 1 (Ackermann's Lemma for ALCOI). Let O be an ALCOIontology, let C be a concept expression and suppose the concept symbol A does not occur in C. Let I be an arbitrary ALCOI-interpretation. (i) If A occurs only positively in O, then I j= OCA i for some interpretation I0 A-equivalent to I, I0 j= A v C; O. (ii) If A occurs only negatively in O then I j= OCA i for some interpretation I0 A-equivalent to I, I0 j= C v A; O. 4
Our forgetting method is called Dsqel, which is short for Description logics Second-order Quanti er ELimination.
Figure 1 outlines the basic routine of the Dsqel method to forget concept symbols in ALCOI-ontologies O. Once receiving the input ontology and a set of concept symbols to forget, the method proceeds as follows. In Phase 1, a preprocessing step is performed to transform the axioms into a set of clauses. This is done by replacing all inclusions C v D by :C t D, and all equivalences C D by :C t D and :D t C. Inexpensive equivalence-preserving syntactic simpli cation rules are also applied in this phase to simplify clauses. For example, C t (C u D) is simpli ed to C. Phase 2 counts the number of positive (and negative) occurrences of each concept symbol in . Using these counts an 1. Transform ontology O to clausal representation N := clause(O). 2. Process every concept symbol A in and check the frequency of A in polarity terms to generate the ordering . 3. Guided by , apply the Dsqel calculus to each of the concept symbols in to produce the ontology O0 (with clauses interpreted in the obvious way as inclusions). 4. Apply the simpli cation rules provided to O0 if needed and return the resultant ontology containing the symbols only in sig(O0)n . ordering is de ned on the symbols in . This ordering determines the order in which the symbols in are eliminated in the next phase. Phase 3 applies the Dsqel calculus described in the next section to the non-base symbols in one by one, starting with the symbol A largest in the ordering . To forget A the inference rules of the Dsqel calculus are applied to the axioms containing A. Then the next largest non-base symbol is eliminated, and so on.
Forgetting a concept symbol may lead to a change of the polarities of the occurrences of the remaining -symbols, and a new elimination order may have to be computed based on the refreshed polarity counts, before the forgetting method to continues. This means Phase 2 and Phase 3 will be alternately and repeatedly executed with recomputed elimination orders. If the largest current concept symbols to be eliminated could not be completely eliminated by Dsqel, then a di erent ordering not attempted before will be used. In the case that all possible orderings have been tried and every attempt to eliminate all non-base symbols using Dsqel is not successful, the method returns failure, because it was unable to solve the problem. On the other hand, when after a call of Dsqel the set returned does not contain any non-base symbols, then this is the result of forgetting from O.
Phase 4 subsequently applies further simpli cation rules and transforms the resulting axioms to simpler representations.
Di erent elimination orders of concept symbols applied may lead to di erent but equivalent results. The results can be viewed (when the remaining non-base symbols are existentially quanti ed) as equivalent representations of 9 O.
What is returned by the algorithm, if it terminates successfully, is a (possibly empty) ontology with all occurrences of the non-base symbols eliminated. I.e., what is returned is an ontology speci ed in terms of only the symbols in sig(O)n .
There are situations where our method does not succeed, for instance, when
no forgetting result nitely expressible in ALCOI exists. This means the method
is not complete, but since no complete method can exist for forgetting, as
considered in this paper, this is to be expected. Concept forgetting is already not
always computable for the description logic E L [
Purify: provided:
N; C1 t A; : : : ; Cn t A (N AC1t:::t Cn ):C:1;C::1:;;C::n:;::Cn (i) A is a non-base symbol, (ii) A does not occur in any of the Ci, (iii) A is strictly maximal wrt. each Ci, and (iv) N is negative with respect to A.
N (N:A>):>:> (i) A is a non-base symbol in N , and (ii) N is negative with respect to A. they are ineliminable. It might be the case that they are eliminable, but simply our method is unable to nd a solution.
We can show Dsqel algorithm is correct and is guaranteed to terminate.
This follows as an adaptation of the correctness and termination of the Msqel
procedure proved in [
The order in which the non-base symbols are eliminated is determined by the ordering computed in Phase 2 of the Dsqel algorithm. We say a concept symbol A is strictly maximal with respect to a concept C if for any concept symbol B (6= A) in C, A B.
A concept C is positive (negative) with respect to a concept symbol A i all occurrences of A in C are positive (negative). A set of concepts N is positive (negative) with respect to a concept symbol A i all occurrences of A in N are positive (negative).
The Ackermann rule and the Purify rule, given in Figure 2, are the forgetting rules in the Dsqel calculus, which will lead to the elimination of a non-base concept symbol. Both of them have to meet particular requirements on the form of the concepts to which they apply. N is a set of ALCOI-clauses, and by NCD, we mean the set obtained from N by substituting the expression C for all occurrences of D in N , where C and D are both ALCOI-concepts. The inference rules in the Dsqel calculus are restricted by a set of side-conditions; for example, the side-conditions of the Ackermann rule require that A must be a non-base symbol and does not occur in C1; : : : ; Cn, no non-base symbol occurring in Ci (1 i n) is larger than A under the ordering , and every occurrence of A in N must be negative. The Purify rule can be seen as a special case of the Ackermann rule, since it eliminates the non-base symbols that occur only negatively, that is, when there are no positive occurrences of A.
Surfacing:
N; C t 8R :D
N; 8R ; :C t D provided: (i) A is the largest non-base symbol in C t 8R :D, (ii) A does not occur in C, and (iii) A occurs positively in 8R :D.
Skolemization:
N; :a t :8R :C N; :a t :8R ::b; :b t
C provided: (i) A is the largest non-base symbol in :a t :8R :C, (ii) A occurs positively in :8R :C, and (iii) b is a new nominal.
Clausify:
N; C t :(D1 t ::: t Dn)
N; C t D1; :::; C t Dn provided: (i) A is the largest non-base symbol in C t :(D1 t ::: t Dn), (ii) A occurs positively in D1 t ::: t Dn.
Sign Switching:
N (N:AA):A:A provided: (i) N is closed with respect to the other rules, (ii) A is the largest non-base symbol in N , and (iii) Sign switching wrt. A has not been performed before.
The rules in Figure 3, are used to rewrite the formulae so they can be
transformed into the form where either the Ackermann rule or the Purify rule is
applicable. To apply these rules, the positive occurrences of the non-base symbol rst
have to be made `individually isolated'. In addition, every positive occurrence
of the non-base symbol must occur at the top level as a literal in a clause [
The Skolemization rule rewrites the existential expression in a clause of the form :a t :8R :C, where a is a nominal. The implicit existential quanti er in :8R :C is Skolemized by introducing a new Skolem constant (nominal) b.
The clausify rule transforms a concept of the form C t :(D1 t ::: t Dn) into a set of clauses.
The Sign switching rule is used to switch the polarity of a non-base symbol. It is applicable only when no other rules in the calculus are applicable with respect to this non-base symbol and the Sign switching rule has not been performed on this non-base symbol before.
Case Splitting:
N; :a t C1 t ::: t Cn
N; :a t C1 j ::: j N; :a t Cn provided: (i) A is the largest non-base symbol in :a t C1 t ::: t Cn, (ii) A occurs positively in C1 t ::: t Cn.
A novelty in the Dsqel calculus is the case splitting inference rule given in Figure 4. It splits a clause of the form :a t C1 t ::: t Cn into smaller subclauses :a t C1, :a t C2, ..., :a t Cn. A single clause :a t C, together with N , forms a case. The original formula means that at least one of the disjuncts Ci (1 i n) is true for a. The bene ts of the case splitting rule are twofold. On the one hand, the case splitting rule makes up for a limitation of the Skolemization rule, because it splits a disjunction with more than two disjuncts into several smaller cases, which the Skolemization rule is able to handle. On the other hand, our tests show it reduces the search space and increases the success rate.
Condensing I:
N C t 8R 1 :8R 1; : : : : 8R n :8R n; :(C t D)
N C t D t 8R 1 ? provided: (i) C and D are arbitrary concepts, and (ii) i 1 for 1 i n
N C t 8R 1 :8R 1; : : : : 8R n :8R n; :(C t D)
N C t D t 8R n ? provided: (i) C and D are arbitrary concepts, and (ii) i n for 1 i n
Fig. 5. Sample simpli cation rule
We also introduced several simpli cation rules to transform more expressions so that inference rules become applicable, they keep expressions in simpler forms for e ciency, and most importantly, they lead to success of forgetting in more cases. Figure 5 displays two cases of the simpli cation rules, called Condensing I, with which one can handle clauses of a particular pattern where other existing methods fail. 6
In order to evaluate how the Dsqel method behaves on real-life ontologies, we implemented it in Java using the OWL API and applied the implementation to a set of ontologies from the NCBO BioPortal1, a large repository of biomedical ontologies. The experiments were run on a machine with an Intelr Coretm i74790 processor, and four cores running at up to 3.60 GHz and 8 GB of DDR31600 MHz RAM.
Since Dsqel handles expressivity as far as ALCOI, the ontologies for our evaluation were restricted to their ALCOI-fragments, and axioms outside of the scope of ALCOI were dropped from the ontologies. Consequently, we used 292 ontologies from the repository for our evaluation. We ran the experiments on each ontology 100 times and averaged the results to explore how forgetting was in uenced by the number of the concept symbols in an ontology. A timeout of 1000 seconds was used.
To t with possible needs of applications, we conducted experiments where we forget 10%, 30%, and 50% of the concept symbols in the ontologies. The Dsqel algorithm processes each non-base symbol and counts the number of their positive (and negative) occurrences. Based on these counts, an elimination order is generated by a heuristic algorithm. In order to see how the elimination order a ects the performance of the calculus, we ran two sets of experiments, where we omitted the analysis of the elimination order for one set, and applied the analysis to the other set. The evaluation results with respect to forgetting 10%, 30%, 50% of the concept symbols in the ontologies, without and with the analysis of the elimination order, are shown in Table 1.
It can be seen that, the analysis of the elimination order leads to a decrease in the average duration of the runs of every experiment, which means that it takes shorter time to complete the same task than when analysis of the elimination order is not performed. It is evident that the analysis for the elimination order has brought a positive e ect on the overall success rate (increase by 8.1%) and the timeout rate (decrease by 5.9%).
Evaluations of more aspects are being conducted at the moment. These
evaluations are focussed on, for example, how the case splitting rule makes a di erence
to the behaviour of the Dsqel calculus, and how our method compares to the
related methods of Scan [
It has been shown that the Scan algorithm is complete and terminates for
modal axioms belonging to the famous Sahlqvist class [
Investigation of forgetting as uniform interpolation in more expressive
description logics was started in [
We have presented a second-order quanti er elimination method, called Dsqel, for forgetting concept symbols in ontologies speci ed in the description logic ALCOI.
It is adapted from Msqel, an Ackermann-based second-order quanti er elimination method for a multi-modal tense logic with second-order quanti cation. The method is enhanced with new inference and simpli cation rules. The adaptation was motivated for the purpose of applying the second-order quanti er elimination techniques to the area of knowledge representation, where description logics provide important logical formalisms.
We have had a prototype implementation of our forgetting method, fully realising the Dsqel method. It is known that the success of a forgetting problem is highly dependent on, apart from the calculus itself, the non-base symbols to be forgotten, and the elimination order which the method follows. The evaluation results of rst experiments reported in this paper show promising and very good success rates for concept symbol forgetting.
Optimisation to both the calculus and the implementation is underway. One optimisation being investigated is the incorporation of more simpli cation rules in order to increase the e ciency and success rate further. We are also currently working on nding a heuristic algorithm using a dynamic way of ordering the non-base symbols, because the elimination of a particular concept symbol may a ect the optimality of the elimination order, and thus computing a new order may be bene cial. Research shows that the order in which the inference rules are applied is signi cant because, as we observed, it is a main factor a ecting the e ciency of the method.
Extending the method to handle ontologies going expressively further than ALCOI is a direction of the ongoing research. To explore how the forgetting of role symbols can be incorporated into our method is also of interest.