=Paper=
{{Paper
|id=Vol-1350/paper-39
|storemode=property
|title=Concept
Forgetting for ALCOI-Ontologies using an Ackermann Approach
|pdfUrl=https://ceur-ws.org/Vol-1350/paper-39.pdf
|volume=Vol-1350
|dblpUrl=https://dblp.org/rec/conf/dlog/ZhaoS15
}}
==Concept
Forgetting for ALCOI-Ontologies using an Ackermann Approach==
https://ceur-ws.org/Vol-1350/paper-39.pdf
Concept Forgetting in ALCOI-Ontologies using
an Ackermann Approach
Yizheng Zhao and Renate A. Schmidt
The University of Manchester, UK
Abstract. We present a method for forgetting concept symbols in on-
tologies specified in the description logic ALCOI. The method is an
adaptation and improvement of a second-order quantifier elimination
method developed for modal logics and used for computing correspon-
dence properties for modal axioms. It follows an approach exploiting a
result of Ackermann adapted to description logics. Important features in-
herited from the modal approach are that the inference rules are guided
by an ordering compatible with the elimination order of the concept sym-
bols. This provides more control over the inference process and reduces
non-determinism, and the size of the search space. The method is ex-
tended with a new case splitting inference rule, and several simplification
rules. Compared to related forgetting and uniform interpolation meth-
ods 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 efficient in time and has higher success rates. The method has been
implemented in Java using the OWL API. Preliminary experimental re-
sults show that the order in which the concept symbols are eliminated
significantly affects the success rate and efficiency.
1 Introduction
Ontology-based technologies provide novel ways of building knowledge process-
ing systems and play an important role in many different 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 het-
erogeneous. 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 different 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 beneficial 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 specific, to create a sum-
mary of the ontology [29]. Situations where ontologies are published, shared, or
disseminated, but some sensitive parts described in terms of particular signature
symbols needs to be kept confidential or unseen to the receiver, is a potential
application of forgetting [3]. This is relevant for medical and military uses, and
uses in industry to ensure proprietary information can be kept hidden.
The contribution of this paper is the presentation of a method for forgetting
concept symbols in ontologies specified 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 [31] and EL [20, 22]
and EL-extensions [11], to more expressive ones, such as ALC [21, 30, 19, 14, 13],
ALCH [12], SIF [17] and SHQ [15].
Forgetting can however also be viewed as a second-order quantification prob-
lem, which is the view we take in this paper. In second-order quantifier elimina-
tion, the aim is to eliminate existentially quantified predicate symbols in order
to translate second-order formulae into equivalent formulae in first-order logic [5,
6, 8, 4, 7, 26, 23, 24, 28]. In uniform interpolation the aim is to eliminate symbols
too, though it is not required that the result is logically equivalent to the cor-
responding formula in second-order logic, only that all important consequences
are preserved.
Our method is adapted from a method, called Msqel, designed for modal
logic to compute first-order frame correspondence properties for modal axioms
and rules [26]. The adaptation exploits the close relationship between descrip-
tion logics and modal logics [25]. Our method contributes three novel aspects.
It is the first method for forgetting concept symbols from ontologies specified
in the description logic ALCOI. It inherits from Msqel the consideration of
elimination orders, which has been shown to improve the success rate and make
it succeed on a wider range for problems in the modal logic corresponding to
ALCOI [26]. The success rate and its scope is further improved by the incorpo-
ration of a new case splitting rule and generalised simplification rules. Results of
an empirical evaluation show improved success rates and performance for these
techniques.
2 Definition of ALCOI and Other Basic Definitions
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 | ⊥ | > | A | ¬C | C t D | C u D | ∃R.C | ∃R− .C | ∀R.C | ∀R− .C,
where a ∈ NO , A ∈ NC , R ∈ NR , and C and D are arbitrary ALCOI-concepts.
R− denotes the inverse of the role R. By definition, 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 definition 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 ∃R.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 define 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 ∈
NO a singleton set aI ⊆ ∆I ; to every concept symbol A ∈ NC a subset AI
of ∆I ; and to every role symbol R ∈ NR a subset RI of ∆I × ∆I . We specify
the semantics of ALCOI-concepts by extending the interpretation function to
the following:
⊥I = ∅ (¬C)I = ∆I \C I (C t D)I = C I ∪ DI
(∀R.C)I = {x ∈ ∆I | ∀y.(x, y) ∈ RI → y ∈ C I }
(∃R.C)I = {x ∈ ∆I | ∃y.(x, y) ∈ RI ∧ y ∈ C I }
(R− )I = {(y, x) ∈ ∆I × ∆I | (x, y) ∈ RI }
The semantics of the TBox-axioms is defined as follows: an interpretation I
satisfies C v D iff C I ⊆ DI , and I satisfies C ≡ D iff C I ≡ DI . If O is a set
of TBox axioms, I is a model of O iff it satisfies every axiom in O, denoted by
I |= O.
In the rest of the paper, we also need the following definitions. A clause is a
disjunction of ALCOI-concepts. Let A be a concept symbol and let I and I 0 be
interpretations. We say I and I 0 are A-equivalent, if I and I 0 coincide but differ
possibly in the valuation assigned to A. This means their domains coincide, i.e.,
0 0
∆I = ∆I , and for each symbol s in the signature except for A, sI = sI . More
generally, suppose Σ = {A1 , . . . , Am } ⊆ NC , I and I 0 are Σ-equivalent, if I
and I 0 are the same but differ possibly in the valuations assigned to the concept
symbols in Σ.
3 Forgetting as Second-Order Quantifier Elimination
We are interested in forgetting concept symbols in axioms of an ontology O of
TBox axioms. Let sig(O) denote the signature of O.
Definition 1. Let O and O0 be ALCOI-ontologies and let Σ = {A1 , . . . , Am } be
a set of concept symbols. O0 is the result of forgetting the symbols in Σ from O,
if sig(O0 ) ⊆ sig(O)\Σ and for any interpretation I,
I |= O iff I 0 |= O0 for some interpretation I 0 Σ-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)\Σ as the base symbols. The result
of forgetting a concept symbol A from O is the result of forgetting {A} from O.
The result of forgetting a symbol A from an ontology O can be represented
A
as ∃X OX in the extension of the language with existentially quantified concept
A
variables. OX 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 quantification of predicate symbols, the
result of forgetting always exists. The challenge of forgetting, as a computational
problem, is to find an ontology O0 (without any occurrences of X) in the source
A
language (without second-order quantification) that is equivalent to ∃X OX ,
0
where O is expressed in the source language. Finding such an ontology O that
A
is equivalent to ∃X OX is an instance of the second-order quantifier elimination
problem. Forgetting a concept symbol A is thus the problem of eliminating the
A
existential quantifier ∃X from ∃X OX . In the following, we slightly informally
say the aim is to eliminate the symbol A from O. For this we apply second-order
quantifier 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 [1], which is known as Ackermann’s Lemma in the literature on
second-order quantifier elimination [8].
Theorem 1 (Ackermann’s Lemma for ALCOI). Let O be an ALCOI-
ontology, 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 |= OCA
iff for some interpretation I 0 A-equivalent
0 A
to I, I |= A v C, O. (ii) If A occurs only negatively in O then I |= OC iff for
0 0
some interpretation I A-equivalent to I, I |= C v A, O.
4 The Forgetting Method DSQEL
Our forgetting method is called Dsqel, which is short for Description logics
Second-order Quantifier 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
simplification rules are also applied in this phase to simplify clauses. For ex-
ample, C t (C u D) is simplified 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 simplification rules provided to O0 if needed and return the
resultant ontology containing the symbols only in sig(O0 )\Σ.
Fig. 1. The phases in the basic Dsqel routine
ordering is defined 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 different 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 simplification rules and transforms the
resulting axioms to simpler representations.
Different elimination orders of concept symbols applied may lead to different
but equivalent results. The results can be viewed (when the remaining non-base
symbols are existentially quantified) as equivalent representations of ∃Σ O.
What is returned by the algorithm, if it terminates successfully, is a (pos-
sibly empty) ontology with all occurrences of the non-base symbols eliminated.
I.e., what is returned is an ontology specified in terms of only the symbols in
sig(O)\Σ.
There are situations where our method does not succeed, for instance, when
no forgetting result finitely expressible in ALCOI exists. This means the method
is not complete, but since no complete method can exist for forgetting, as con-
sidered in this paper, this is to be expected. Concept forgetting is already not
always computable for the description logic EL [10]. We also note that concept
symbols cannot be eliminated by our method does not necessarily mean that
N, C1 t A, . . . , Cn t A
Ackermann: A
(N∼C )¬¬C1 ,...,¬¬Cn
1 t...t∼Cn C1 ,...,Cn
provided: (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
Purify: A ¬¬>
(N¬> )>
provided: (i) A is a non-base symbol in N , and
(ii) N is negative with respect to A.
Fig. 2. The elimination rules
they are ineliminable. It might be the case that they are eliminable, but simply
our method is unable to find 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 [26], since all adaptations of Msqel to Dsqel preserve
logical equivalence and the calculus given in the next section is correct and
terminates.
5 The DSQEL Forgetting Calculus
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 iff all
occurrences of A in C are positive (negative). A set of concepts N is positive
(negative) with respect to a concept symbol A iff 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.
N, C t ∀Rσ .D
Surfacing:
N, ∀Rσ,− .C t D
provided: (i) A is the largest non-base symbol in C t ∀Rσ .D,
(ii) A does not occur in C, and
(iii) A occurs positively in ∀Rσ .D.
N, ¬a t ¬∀Rσ .C
Skolemization:
N, ¬a t ¬∀Rσ .¬b, ¬b t ∼C
provided: (i) A is the largest non-base symbol in ¬a t ¬∀Rσ .C,
(ii) A occurs positively in ¬∀Rσ .C, and
(iii) b is a new nominal.
N, C t ¬(D1 t ... t Dn )
Clausify:
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 .
N
Sign Switching: A ¬¬A
(N¬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.
Fig. 3. The rewriting rules
The rules in Figure 3, are used to rewrite the formulae so they can be trans-
formed into the form where either the Ackermann rule or the Purify rule is appli-
cable. To apply these rules, the positive occurrences of the non-base symbol first
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 [26],
that is, they must not occur under a quantifier restriction operator or any other
logical operator except for disjunction. This is done by repeatedly using the sur-
facing rule. By Rσ , we mean the composition of a sequence of roles and by Rσ,−
we mean the composition of the sequence of inverses of the roles in Rσ with the
order in the sequence reversed.
The Skolemization rule rewrites the existential expression in a clause of the
form ¬a t ¬∀Rσ .C, where a is a nominal. The implicit existential quantifier in
¬∀Rσ .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.
N, ¬a t C1 t ... t Cn
Case Splitting:
N, ¬a t C1 | ... | 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 .
Fig. 4. The case splitting rule
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 benefits 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.
N C t ∀Rσ1 .∀Rσ1 ,− . . . . ∀Rσn .∀Rσn ,− .(C t D)
Condensing I:
N C t D t ∀Rσ1 ⊥
provided: (i) C and D are arbitrary concepts, and
(ii) σ i ≤ σ 1 for 1 ≤ i ≤ n
N C t ∀Rσ1 .∀Rσ1 ,− . . . . ∀Rσn .∀Rσn ,− .(C t D)
N C t D t ∀Rσn ⊥
provided: (i) C and D are arbitrary concepts, and
(ii) σ i ≤ σ n for 1 ≤ i ≤ n
Fig. 5. Sample simplification rule
We also introduced several simplification rules to transform more expressions
so that inference rules become applicable, they keep expressions in simpler forms
for efficiency, and most importantly, they lead to success of forgetting in more
cases. Figure 5 displays two cases of the simplification rules, called Condensing I,
with which one can handle clauses of a particular pattern where other existing
methods fail.
6 Empirical Results
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 i7-
4790 processor, and four cores running at up to 3.60 GHz and 8 GB of DDR3-
1600 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
influenced by the number of the concept symbols in an ontology. A timeout of
1000 seconds was used.
To fit 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 affects 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 effect 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 evalu-
ations are focussed on, for example, how the case splitting rule makes a difference
to the behaviour of the Dsqel calculus, and how our method compares to the
related methods of Scan [7], Dls [5], Dls∗ [6], Sqema [4], Msqel [26], and
LETHE [16] for computing uniform interpolants, in terms of the success rate
and efficiency (duration and timeouts).
1
http://bioportal.bioontology.org/
Input Experiment Output
Axioms Avg. Symbols Avg. Percentage Order Timeouts Duration Avg. Success Rate
7 3.8% 4.509 sec. 90.1%
10%
3 1.7% 2.404 sec. 97.6%
7 7.5% 8.562 sec. 88.4%
1407 876 30%
3 2.2% 2.753 sec. 95.5%
7 13.4% 15.068 sec. 85.3%
50%
3 3.1% 3.004 sec. 94.9%
7 8.2% 9.380 sec. 87.9%
1407 876 Average
3 2.3% 2.720 sec. 96.0%
Table 1. Forgetting 10%, 30%, and 50% of concept symbols in ontologies
7 Related Work
Probably the most important early work on the elimination of second-order quan-
tifiers is that of Ackermann [1] in 1935. Only in 1992, Gabbay and Ohlbach [7]
developed the first practical algorithm, called Scan. Scan is a resolution-based
second-order quantifier elimination algorithm and can be used to forget predicate
symbols from first-order logic formulae [24].
It has been shown that the Scan algorithm is complete and terminates for
modal axioms belonging to the famous Sahlqvist class [9]. In 1994, the hier-
archical theorem proving method was developed by Bachmair et al. [2] and it
has been shown that it can be used to solve second-order quantification prob-
lems. Around the same time, in 1995, Szalas [27] described a different algorithm
for the second-order quantifier elimination problem, which exploits Ackermann’s
Lemma. The method was further extended to the Dls algorithm by Doherty et
al. [5]. Dls uses a generalised version of Ackermann’s Lemma and allows the
elimination of existential second-order quantifiers from second-order formulae,
and obtaining corresponding first-order equivalents. Nonnengart and Szalas [23]
generalised the main result underlying the Dls algorithm to include fixpoints.
Based on this work, Doherty et al. [6] proposed the Dls∗ algorithm, which at-
tempts the derivation of either an equivalent first-order formula or a fixpoint
formula from the original formula. Dls and Dls∗ are Ackermann-based second-
order quantifier elimination methods. Ackermann-based second-order quantifier
elimination was first applied to description logics in [28] by Szalas, where descrip-
tion logics were extended by a form of second-order quantification over concepts.
More recently, Conradie et al. [4] introduced the Sqema algorithm, which is also
an Ackermann-based method but for modal logic formulae. It is specialised to
find correspondences between modal formulae and hybrid modal logic formu-
lae (and first-order formulae). Schmidt [26] has extended Sqema and developed
Msqel as a refinement. A key novelty is the use of elimination orders, and the
presentation of second-order quantifier elimination as an abstract calculus.
Investigation of forgetting as uniform interpolation in more expressive de-
scription logics was started in [29] and [21]. The first approach to compute uni-
form interpolations for ALC-TBoxes was presented in [29]. It is a tableau-based
approach, where a disjunctive normal form is required for the representation of
the TBox-axioms and the uniform interpolants are incrementally approximated.
It was shown in [21] that deciding the existence of uniform interpolants that
can be finitely represented in ALC without fixpoints is 2-ExpTime-complete
and in the worst case, the size of uniform interpolants is triple exponential with
respect to the size of the original TBox. The first goal-oriented method based
on clausal resolution was presented in [19] for computing uniform interpolants
of ALC-TBoxes, where experimental results show the practicality for real-life
ontologies. Koopmann and Schmidt presented another resolution-based method
exploiting structural transformation to compute uniform interpolants of ALC-
ontologies, which uses fixpoint operators to make uniform interpolants finitely
representable [14]. The method has been further extended to handle ALCH [12],
SIF [17], SHQ [15], and ALC with ABoxes [18].
8 Conclusion and Future Work
We have presented a second-order quantifier elimination method, called Dsqel,
for forgetting concept symbols in ontologies specified in the description logic
ALCOI.
It is adapted from Msqel, an Ackermann-based second-order quantifier elim-
ination method for a multi-modal tense logic with second-order quantification.
The method is enhanced with new inference and simplification rules. The adap-
tation was motivated for the purpose of applying the second-order quantifier
elimination techniques to the area of knowledge representation, where descrip-
tion 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 first 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 simplification rules
in order to increase the efficiency and success rate further. We are also currently
working on finding a heuristic algorithm using a dynamic way of ordering the
non-base symbols, because the elimination of a particular concept symbol may
affect the optimality of the elimination order, and thus computing a new order
may be beneficial. Research shows that the order in which the inference rules
are applied is significant because, as we observed, it is a main factor affecting
the efficiency 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.
References
1. W. Ackermann. Untersuchungen über das Eliminationsproblem der mathematis-
chen Logik. Mathematische Annalen, 110(1):390–413, 1935.
2. L. Bachmair, H. Ganzinger, and U. Waldmann. Refutational theorem proving for
hierarchic first-order theories. Applicable Algebra in Engineering, Communication
and Computing, 5(3-4):193–212, 1994.
3. C. Bernardo and B. Motik. B.: Reasoning over ontologies with hidden content: The
importby-query approach. J. Artificial Intelligence Research, 45:197–255, 2012.
4. W. Conradie, V. Goranko, and D. Vakarelov. Algorithmic correspondence and
completeness in modal logic. I. the core algorithm SQEMA. Logical Methods in
Computer Science, 2(1), 2006.
5. P. Doherty, W. Lukaszewicz, and A. Szalas. Computing circumscription revisited:
A reduction algorithm. Journal of Automated Reasoning, 18(3):297–336, 1997.
6. P. Doherty, W. Lukaszewicz, and A. Szalas. General domain circumscription and
its effective reductions. Fundam. Inf., 36(1):23–55, 1998.
7. D. M. Gabbay and H. J. Ohlbach. Quantifier elimination in second–order predicate
logic. In Principles of Knowledge Representation and Reasoning (KR92), pages
425–435. Morgan Kaufmann, 1992.
8. D. M. Gabbay, R. A. Schmidt, and A. Szalas. Second Order Quantifier Elimination:
Foundations, Computational Aspects and Applications. College Publications, 2008.
9. V. Goranko, U. Hustadt, R. A. Schmidt, and D. Vakarelov. SCAN is complete for
all sahlqvist formulae. In Relational and Kleene-Algebraic Methods in Computer
Science, volume 3051 of Lecture Notes in Computer Science, pages 149–162, 2004.
10. B. Konev, C. Lutz, D. Walther, and F. Wolter. Model-theoretic inseparability and
modularity of description logic ontologies. Artificial Intelligence, 203(0):66–103,
2013.
11. B. Konev, D. Walther, and F. Wolter. Forgetting and uniform interpolation in
extensions of the description logic EL. In Proceedings of the 22nd International
Workshop on Description Logics (DL 2009), Oxford, UK, 2009.
12. P. Koopmann and R. A. Schmidt. Forgetting concept and role symbols in ALCH-
ontologies. In Logic for Programming, Artificial Intelligence, and Reasoning, vol-
ume 8312 of Lecture Notes in Computer Science, pages 552–567. Springer, 2013.
13. P. Koopmann and R. A. Schmidt. Implementation and evaluation of forgetting
in ALC-ontologies. In Proceedings of the 7th International Workshop on Modu-
lar Ontologies (WoMo 2013), volume CEUR-WS/Vol-1081 of CEUR Workshop
Proceedings, pages 1–12. CEUR-WS.org, 2013.
14. P. Koopmann and R. A. Schmidt. Uniform interpolation of ALC-ontologies using
fixpoints. In Frontiers of Combining Systems, volume 8152 of Lecture Notes in
Computer Science, pages 87–102. Springer, 2013.
15. P. Koopmann and R. A. Schmidt. Count and forget: Uniform interpolation of
SHQ-Ontologies. In Automated Reasoning - IJCAR 2014. Proceedings, pages 434–
448. Springer, 2014.
16. P. Koopmann and R. A. Schmidt. LETHE: A saturation-based tool for non-
classical reasoning, 2015. Manuscript, submitted.
17. P. Koopmann and R. A. Schmidt. Saturation-based forgetting in the description
logic SIF , 2015. This volume.
18. P. Koopmann and R. A. Schmidt. Uniform interpolation and forgetting ALC-
ontologies with aboxes. In Proceedings of AAAI Conference on Artificial Intelli-
gence, pages 175–181, 2015.
19. M. Ludwig and B. Konev. Towards practical uniform interpolation and forgetting
for ALC tboxes. In Proceedings of the 26th International Workshop on Descrip-
tion Logics (DL-2013), volume 1014 of CEUR-WS, pages 377–389. CEUR-WS.org,
2013.
20. C. Lutz, I. Seylan, and F. Wolter. An automata-theoretic approach to uniform in-
terpolation and approximation in the description logic EL. In Principles of Knowl-
edge Representation and Reasoning: KR 2012. AAAI Press, 2012.
21. C. Lutz and F. Wolter. Foundations for uniform interpolation and forgetting in
expressive description logics. In Proceedings of IJCAI 2011, pages 989–995. IJ-
CAI/AAAI, 2011.
22. N. Nikitina. Forgetting in general EL terminologies. In Description Logics, volume
745 of CEUR Workshop Proceedings. CEUR-WS.org, 2011.
23. A. Nonnengart and A. Szalas. A fixpoint approach to second-order quantifier
elimination with applications to correspondence theory. 24:307–328, 1999.
24. H. J. Ohlbach. SCAN—elimination of predicate quantifiers. In M. A. McRob-
bie and J. K. Slaney, editors, Automated Deduction: In proceedings of CADE-13,
volume 1104 of Lecture Notes in Artificial Intelligence, pages 161–165. Springer,
1996.
25. K. Schild. A correspondence theory for terminological logics: Preliminary report.
In Proceedings of IJCAI’91, pages 466–471. Morgan Kaufmann, 1991.
26. R. A. Schmidt. The Ackermann approach for modal logic, correspondence theory
and second-order reduction. Journal of Applied Logic, 10(1):52–74, 2012.
27. A. Szalas. On the correspondence between modal and classical logic: an automated
approach. Journal of Logic and Computation, 3:605–620, 1993.
28. A. Szalas. Second-order reasoning in description logics. Journal of Applied Non-
Classical Logics, 16(3-4):517–530, 2006.
29. K. Wang, Z. Wang, R. Topor, J. Pan, and G. Antoniou. Concept and role forgetting
in ALC ontologies. In The Semantic Web - ISWC 2009, volume 5823 of Lecture
Notes in Computer Science, pages 666–681. Springer, 2009.
30. K. Wang, Z. Wang, R. Topor, J. Z. Pan, and G. Antoniou. Eliminating concepts and
roles from ontologies in expressive description logics. Computational Intelligence,
30(2):205–232, 2014.
31. Z. Wang, K. Wang, R. Topor, and J. Pan. Forgetting for knowledge bases in DL-
lite. In The Semantic Web: Research and Applications, volume 5021 of Lecture
Notes in Computer Science, pages 245–257. Springer, 2008.