Generalized closed world reasoning allows for the assumption of a speci ed maximal set of negated atomic assertions retaining the consistency of an inde nite knowledge base. In this paper, a generalized closed world assumption (GCWA) is speci ed for the description logic ALCN and all of its sublanguages, provided that the terminological component is eliminable. In certain situations, by applying the GCWA, queries are often answered as intended by users. Opposed to queries with an epistemic operator K, querying with this approach provides the information which of the corresponding assertions can consistently be assumed to be true. Further, the GCWA can be applied locally.
The set of assertions logically entailed by a knowledge base usually contains less
elements than expected by users. In description logics (DLs), this is the case for
queries involving value restrictions 8R:C (resp. negated existential restrictions),
at-most restrictions ( n R:C) (resp. negated at-least restrictions) or atomic
negation :A resp. :R. For example, 8hasChild :Female(john) is not entailed
from KB = fhasChild (john; mary ); Female(mary )g, though often intended. Due
to the open world assumption (OWA) of logical formalisms, an assertion is only
entailed if it is satis ed in all models of a knowledge base. An approach to solve
this problem is the closed world assumption (CWA) de ned by Reiter in [
In less expressive DLs equivalent to sets of Horn clauses such as AL0
knowledge bases [
Unfortunately, inde nite knowledge bases (augmenting e.g. AL0 with disjunction or existential quanti cation) do not remain consistent by applying the CWA. Given e.g. a knowledge base KB = f(Intelligent t Rich)(john)g, under CWA John is not intelligent as well as not rich, leading to an inconsistency.
A well-established approach to enable closed world reasoning and to avoid such inconsistencies is to extend the query language with the epistemic operator K [5{7]. With this operator it is possible to apply a concept closure resp. a role closure by using the expression :KA instead of :A, :KR instead of :R, 8KR:C instead of 8R:C and ( n KR:C) instead of ( n R:C). The speci cation of these expressions is similar to the application of a local CWA and therefore of particular importance for querying DL systems. However, there is no information about which assertions can consistently be assumed. Consider again KB = f(Intelligent t Rich)(john)g. Since Intelligent (john) and Rich(john) are not satis ed in all models of KB, :KIntelligent (john) as well as :KRich(john) are entailed from KB though KB [ f:Intelligent (john); :Rich(john)g would be inconsistent. In other words, by executing epistemic queries, there is also the problem of considering inde nite knowledge.
A suitable formalism to deal with disjunctive information is the generalized
closed world assumption (GCWA) [
The main contribution of this paper is the speci cation of a local GCWA for ALCN and all of its sublanguages, provided that the terminological component is eliminable, i.e., a speci cation of a method deciding whether KB j=GCWA holds, where KB = T [ A is an ALCN knowledge base (with the possibility to eliminate T at the beginning of the reasoning process), is an ALCN -assertion and j=GCWA is an entailment relation applying a GCWA only to speci c parts of the domain. Since the GCWA is de ned under consideration of clauses, all assertions involved in KB as well as the assertion are transformed to a propositional clause form. For the transformation of role restrictions, a kind of domain closure is required. In order to deal with existential quanti ers, this domain closure is extended with new constants.
The method presented provides a foundation to apply closed world
reasoning to all further expressive DLs having the nite model property. At the best
of the authors knowledge, until now there has not been a concrete speci cation
of a closed world assumption for DLs composed of basic constructors such as
disjunction, existential quanti cation or non-atomic negation. The approach is
related to formalisms introducing circumscription to DLs [
The approach presented here is also appropriate for users not experienced with non-monotonic DLs: Besides the DL KB and the query speci ed as usual, it only requires the determination of the parts of the domain to be closed.
The paper is structured as follows: In Sect. 2, the syntax and semantics of ALCN is presented. Problems with the CWA are mentioned in Sect. 3 leading to the consideration of the GCWA (Sect. 4). In Sect. 5, the need for an extended domain closure is explained. Sect. 6 shows how ALCN -assertions can be transformed to a propositional clause form with respect to this domain closure and proposes an algorithm for deciding whether an ALCN -assertion is entailed from an ALCN knowledge base under consideration of a local GCWA. The paper concludes in Sect. 7 with a summary and a discussion of the results. 2
The vocabulary of description-logic languages consists of concepts, roles and constants. Based on atomic concepts A and atomic roles R, ALCN concept descriptions C; D are de ned according to the syntax rule C; D ! > j ? j A j :C j (C u D) j (C t D) j 8R:C j 9R:C j ( n R) j ( n R).
Descriptions are constructed with the logical constants > and ?, complements :C, conjunctions (C u D), disjunctions (C t D), value restrictions 8R:C, existential restrictions 9R:C and number restrictions ( n R) and ( n R).
The semantics is de ned with interpretations I = (4I ; I ), where 4I is a non-empty set of all objects considered in I (called the domain of I) and I is an interpretation function which maps constants a to objects of the domain, aI 2 4I , atomic concepts A to subsets of the domain, AI 4I , and atomic roles R to subsets of the cartesian product of the domain, RI 4I 4I . The extension of I to arbitrary ALCN concept descriptions is de ned as follows, where card is a function assigning to a set its cardinality: >I = 4I ?I = ; (:C)I = 4I n CI (C u D)I = CI \ DI (C t D)I = CI [ DI (8R:C)I = fu 2 4I j (8v) [(u; v) 2 RI ! v 2 CI ]g (9R:C)I = fu 2 4I j (9v) [(u; v) 2 RI ^ v 2 CI ]g ( n R)I = fu 2 4I j cardfv j (u; v) 2 RI g ng ( n R)I = fu 2 4I j cardfv j (u; v) 2 RI g ng
An ALCN knowledge base KB = T [ A is comprised of a TBox T and an ABox A. T consists of a set of axioms C v D and C D called concept inclusions resp. concept equivalences and A consists of a set of concept assertions C(a) and role assertions R(a; b), where a and b are constants. An interpretation I satis es C v D resp. C D resp. C(a) resp. R(a; b) if C I D I resp. C I = D I resp. aI 2 C I resp. (aI ; bI ) 2 RI . If an interpretation I satis es all axioms of T resp. all assertions of A it is called a model of T resp. A. If it satis es both T and A it is called a model of KB. Finally, if there is a model of KB, then KB is called satis able.
In the following, the set of all predicate names (i.e. atomic concepts A and
atomic roles R) appearing in a given KB is denoted with PR and the set of
all assertions A(a) and R(a; b) constructable from PR and the constants of KB
with AS. In order to get a basis for the application of a GCWA to DLs, it is
assumed that T is acyclic and does only contain concept inclusions and concept
equivalences of the form A v C resp. A C . Consequently, it is possible to
eliminate T at the beginning of any reasoning process [
A reasoning service relevant for this investigation is the assertion check, symbolically KB j=R , deciding if an assertion is entailed from an ALCN knowledge base KB with respect to an entailment relation j=R (KB j= , if is satis ed in all models of KB). This service provides the basis for querying DL knowledge bases. If = C(a), it is called instance check and if = R(a; b), it is called relation check. Additionally, by a slight extension of the query language, it is possible to decide negated relation checks KB j=R :R(a; b). We will also consider the case in which is a propositional expression (note that j=R is not restricted to relate (sets of) formulas of the same representation language). 3
The CWA has been introduced by Reiter in [
CWA(KB) = f:p j p 2 AS and KB 6j= pg is the closed world assumption of KB. The entailment relation j=cwa considering this assumption for any assertion is de ned by
KB j=cwa i
KB+ j= ; with KB+ = KB [ CWA(KB).
With the CWA, there are no gaps in the knowledge base, since for each atomic
assertion p 2 AS either KB j=cwa p or KB j=cwa :p is successful. The same
holds for arbitrary boolean assertions, but not for assertions with quanti ers
: :
until a domain closure axiom DCA(KB) = (8x) [x = c1 _ ::: _ x = cm] has been
applied [
1. A clause L1 _ ::: _ Ln is a disjunction of literals Li of the form pi or :pi.1
2. A Horn clause is a clause with at most one positive literal.
3. An inde nite clause is a positive clause p1 _ ::: _ pn with n > 1.
In the context of rst-order logic, Reiter [
As a consequence, DL KBs with concept disjunction generally do not remain consistent by applying the CWA: If KB = f(Intelligent t Rich)(john)g, then KB 6j= Intelligent (john), KB 6j= Rich(john) and KB j= Intelligent (john) _ Rich(john).
Consider 9R:>(a) 2 KB. It is known that the constant a is related over R
to an unknown role ller !, usually referred to as a Skolem constant. Minker [
The GCWA [
f:p j p 2 AS ; K 2 PK ; KB 6j= p; and if KB j= p _ K ; then KB j= K g is the generalized closed world assumption of KB. The entailment relation j=gcwa considering this assumption for any assertion is de ned by
KB j=gcwa i KB j= with KB = KB [ GCWA(KB).
Minker suggests that a literal of an inde nite clause can consistently be assumed to be false if there is a subclause without this literal. For example, in the context of propositional logic, KB = fp1; p1 _ p2; p3 _ p4g can consistently be augmented with f:p2g (while KB+ = KB [ f:p2; :p3; :p4g is inconsistent).
A consequence of retaining the consistency is that inde nite knowledge bases under the GCWA are not assumed to be complete: There can be assertions with KB 6j=gcwa and KB 6j=gcwa : . Another property of the GCWA is its relation to the CWA: If KB+ is consistent, then KB = KB+. 1 In this investigation, a clause is always considered to be ground, i.e., only containing variable-free literals.
Since the domain closure axiom solely considers constants c1; :::; cm mentioned in a knowledge base, Skolem constants ! can be identi ed only with these constants such that the interpretation of ! is ! =: c1 _ ::: _ ! =: cm. A consequence of this is that the set of models of a given knowledge base is possibly reduced to unintended models, resulting in unexpected inferences: Suppose KB1 = fHuman(john); 9hasChild :>(john)g and DCA(KB1 ) = (8x )[x =: john]. Then there is only one \absurd" model in which John is a human and a child of himself such that KB1 [ DCA(KB1) j= hasChild(john; john). In addition, it is possible to construct a knowledge base that is inconsistent with the domain closure: If KB2 = fHuman(john); Human(susy ); ( 3 hasChild )(john)g is augmented with its domain closure axiom, it is assumed that there are only the two objects denoted by john and susy, but the restriction ( 3 hasChild )(john) requires that there are at least three objects.
To avoid these problems, in this article it is proposed that a Skolem constant ! can also be identi ed with a new constant . Under consideration of such a constant, every Skolem constant !k can be interpreted as follows: : : : !k = c1 _ ::: _ !k = cm _ !k = k (1)
Given an ALCN knowledge base KB, it is not obvious to determine all
Skolem constants associated to existentially quanti ed assertions in KB or even
all implicit assertions related to these Skolem constants. A foundation to solve
this problem is to eliminate T such that KB = AT and to apply the
tableaubased satis ability algorithm for ALCN e.g. presented in [
For querying purposes, there is the need to capture new constants associated to Skolem constants. This is done by augmenting initially empty sets NEW (T ; v ) with k for every role assertion T (v; !k) 2 S(KB). In the case that v itself is a Skolem constant, for each constant p the Skolem constant is identi able with due to (1), the set NEW (T ; p) has to be augmented with the corresponding k. Concerning KB3 e.g. NEW (R; a) = f 1 ; 2 g, NEW (P ; a) = f 3 g and NEW (P ; 2 ) = f 3 g. If a role assertion T (v; !k) is not contained in all ABoxes of the tableau of S(KB), then there are models I of KB in which !k need not be considered. However, since there is an interest in all possibilities, sets NEW (T ; v ) in this case are constructed as above. 2 The modi ed algorithm needing only polynomial space is not considered here. De nition 4 (Extended Domain Closure). Let KB be a satis able DL knowledge base, c1; :::; cm all constants mentioned in KB and f 1; :::; pg the union of all sets NEW (T ; v ). Then
DCA+(KB) = (8x)[x =: c1 _ ::: _ x =: cm _ x =: 1 _ ::: _ x =: p] is the extended domain closure axiom. : : Regarding KB1, under consideration of DCA+(KB1) = (8x)[x = john _ x = 1], hasChild (john; john) is not entailed from KB1, and referring to KB2, under extended domain closure for each !k associated to ( 3 hasChild)(john) a new constant k is introduced such that KB2 remains consistent.
De nition 5 (Extended Unique Name Assumption). Let KB be a DL knowledge base, c1; :::; cm all constants mentioned in KB and 1; :::; p all new constants to be considered from DCA+(KB). Then
UNA+(KB) = f(ci 6 =:: cj ) j 1 f(ci 6=: k) j 1 f( k 6= l) j 1 i < j i m; 1 k < l mg [
k pg [ p, k and l are associated to the same at-least restrictiong is the extended unique name assumption.
Note that by this de nition, new constants k denote new (not necessarily existent) objects, i.e., di erent from all objects denoted by constants mentioned in KB. Therefore, by considering an extended domain closure and a corresponding extended unique name assumption, an assertion 9hasChild :>(john) is interpreted as usually intended, namely to represent the information that John does have a child either known or not known to a knowledge base. 6 6.1
Propositional Clause Form of ALCN -Assertions Arbitrary ALCN concept assertions in negation normal form (NNF)3 can be transformed to a propositional clause form. The transformation of boolean assertions is depicted in Table 1, where u is a constant belonging to DCA+(KB). 3 In NNF, negation occurs only in front of atomic concepts and roles. belonging to DCA+(KB) are considered while for existential assertions 9R:C(u) and ( n R)(u), it su ces to consider the constants c1; :::; cm and one resp. n new constants k. However, new constants associated to a query have to correspond to new constants considered for KB. Therefore, the transformation of existential assertions with respect to a role R and a constant u, besides all constants c1; :::; cm mentioned in KB is applied with exactly the new constants 1; :::; r contained in NEW (R; u). If all constants to be considered are determined, transformations of existential- and all-quanti ed assertions to a propositional (dual) clause form are based on known correspondences of ALCN to rst-order logic (cf. [9, p. 54]) and are depicted in Table 2 resp. Table 3. Note that transformations of assertions with quali ed role restrictions are de ned recursively with respect to C.
For the dual clause form of 9R:C(u) there is an equivalent clause form such that for each ALCN knowledge base KB = AT there is a corresponding set of clauses. Regarding ( n R)(u), jNj is the cardinality of fc1; :::; cm; 1; :::; rg. In the context of a query or in the case that Skolem constants associated to an expression in scope of a value restriction are not introduced (see Sect. 5), it is possible that n >jNj such that ( n R)(u) is equivalent to ?(u). However, in these cases the problems mentioned for KB1 and KB2 in Sect. 5 cannot occur.
: Due to UNA+(KB), axioms v1 6= v2 with arbitrary constants v1; v2 need not be considered by transforming ( n R)(u). Similarly, due to UNA+(KB), only equalities k =: l involving pairs of new constants not associated to the same at-least restriction have to be considered for the transformation of ( n R)(u) (abbreviated with EQ ). Furthermore, if there are less than n + 1 constants belonging to DCA+(KB), then ( n R)(u) is equivalent to >(u). De nition 6. Let KB be an ALCN knowledge base, U the set of all constants belonging to DCA+(KB) and (PR) PR the set of predicates assumed to be speci ed complete. Then j=GCWA for any assertion is de ned by KB j=GCWA i
(GCWA(KB)) [ DCA+(KB) [ UNA+(KB) j= , where (GCWA(KB)) = f:F (u) 2 GCWA(KB) j u 2 U and F 2 (PR)g.
Besides the extended domain closure and its corresponding unique name assumption, with j= GCWA a GCWA is applied locally, i.e., only for predicates F 2 (PR). The AssertALCN algorithm deciding whether KB j=GCWA is depicted in Table 4. Algorithm AssertALCN (KB, , (PR)) input ALCN knowledge base KB = T [ A, ALCN -assertion , set (PR) of predicates assumed to be speci ed complete output TRUE if KB j=GCWA , else FALSE 1. Expand A w.r.t. T such that KB = AT 2. If there is an ALCN tableau proof for KB j=una+ ?(a) for the constant a, evaluate to TRUE and stop 3. Determine all sets NEW (T ; v ) containing new constants k for atomic roles
T and constants v appearing in the full expanded tableau of 2. 4. Transform NNF (KB) under consideration of sets NEW (T ; v ) in a propositional clause form Cl(KB) 5. Compute the set Res(Cl(KB)) by adding to Cl(KB) all resolvents of Cl(KB) 6. Transform NNF ( ) under consideration of sets NEW (T ; v ) in a propositional clause form Cl( ) 7. If there is a clause K 2 Cl( ) neither containing > nor literals L and :L and further not ful lling any of the constraints (a) K or a subclause of K is in Res(Cl(KB)) (b) K contains a negative Literal :A(a) resp. :R(a; b) with A 2 (PR) resp. R 2 (PR) s.t. for all positive clauses of Res(Cl(KB)) containing A(a) resp. R(a; b) there is a subclause in Res(Cl(KB)) without A(a) resp. R(a; b) evaluate to FALSE and stop, else evaluate to TRUE and stop
It is assumed that the reader is familiar with the propositional resolution
calculus. After the elimination of T (1.), KB = AT is checked for satis ability
(2.). GCWA(KB) as well as DCA+(KB) need not be considered for this check,
since these assumptions are known to retain the consistency of KB. But KB is
inconsistent with UNA+(KB), if ( n R)(v), R(v; v1); :::; R(v; vn+1) and vi 6=: vj
for all pairs (vi; vj ) are in S(KB). Therefore the satis ability check is
evaluated with the entailment relation j=una+ considering UNA+(KB). There is no
information whether ci 6 =: !k, and all axioms !k 6 =: !l with pairs of Skolem
constants associated to the same at-least restriction are introduced by the calculus
[
The soundness and completeness of AssertALCN is based on the soundness and completeness of the well-known propositional resolution calculus. Given a set of clauses Cl(KB), a set of clauses Cl( ) is proved with this calculus, symbolically Cl(KB) `Res Cl( ), if an empty clause can be derived from Cl(KB) [ :Cl( ), where :Cl( ) has been transformed to clause form.
Theorem 2. Let K be a non-tautological clause. Then K or a subclause of K is in Res(Cl(KB)) if and only if Cl(KB) `Res K.
Proof. (sketch) Res(Cl(KB)) contains all implicit clauses of Cl(KB). All further resolvents are obtained by the consideration of :K = :L1 ^ ::: ^ :Ln. \)": Consider Cl = L1 _ ::: _ Lk 2 Res(Cl(KB)) with k n. It is obvious that the k-th resolvent of Cl and :K is the empty clause. \(": Consider fg 6`Res K (K is non-tautological), K0 = L01 _ ::: _ L0m 2 Res(Cl(KB)) and there is no subclause of K0 in Res(Cl(KB)). If the negation of only k literals L0i is contained in :K, then the k-th resolvent of K0 and :K consists of all literals L0j whose negation is not contained in :K and there are no further resolvents of Res(Cl(KB)) and :K. Therefore all :L0i must be contained in :K and m must be lower than or equal than n in order to derive the empty clause. tu Since Cl(KB) `Res K1 ^ ::: ^ Kn i Cl(KB) `Res K1; :::; Cl(KB) `Res Kn, all clauses K1; :::; Kn are independent of each other. Consequently, Theorem 2 also holds for a set of clauses Cl( ) such that decisions obtained by executing step 7 (a) are sound and complete. Finally, step 7 (b) exactly corresponds to the consideration of (GCWA(KB)). AssertALCN can further be simpli ed by deleting all superclauses of Res(Cl(KB)). Then, in step 7 (b) it su ces to check if there are positive clauses in Res(Cl(KB)) containing A(a) resp. R(a; b). Example 1. Let KB = f9R:A(a); R(a; b); A(b)g and suppose there is interest in deciding whether KB j=GCWA 8R:A(a) for (PR) = fRg. It is obvious that KB 6j=una+ ?(a). The fact that a itself is mentioned in KB is independent of this.
: :
DCA+(KB) = (8x)[x = a _ x = b], since the 9-rule (cf. [
Example 2. Suppose KB = f8R:A(a); 9R:>(a)g with NEW (R; a) = f 1 g. There is interest in deciding whether KB j=GCWA :A(a) with (PR) = fA; Rg. The clause form of KB is f:R(a; a) _ A(a); :R(a; 1) _ A( 1); R(a; a) _ R(a; 1)g. The resolvents A(a) _ R(a; 1) as well as R(a; a) _ A( 1) can be derived. Since in Res(Cl(KB)) there is the clause A(a) _ R(a; 1), but not the clause R(a; 1), the instance check given above is not successful. 7
We proposed a method for applying a local closed world assumption for DLs including inde nite knowledge which is also appropriate for users not experienced with non-monotonic DLs. As mentioned in the introduction, under the OWA there are often answers to queries that are not intended by users. Referring to the approach presented, these answers are due to the presence of negative literals in the corresponding propositional clause form of the query. By applying the GCWA, a subset of those negative literals whose non-negative counterpart cannot be proven is assumed to be true. This subset in general is strict, since under the GCWA inde nite knowledge remains inde nite, i.e., an inde nite knowledge base under the GCWA is not assumed to contain complete knowledge. Following to this, there are still answers to queries that are not intended by a lot of users.
Further investigations could be adressed to the extension of this approach to DLs more expressive than ALCN as well as to DLs with no restrictions on the terminological component, i.e., allowing for general concept inclusions (GCIs). Though the set Res(Cl(KB)) for each KB has to be determined only once, its computation is highly intractable such that an optimization of the proposed method is of particular importance.
Acknowledgements. Special thanks go to Carola Eschenbach from the University of Hamburg and Ralf Moller from the Hamburg University of Technology.