Autoepistemic Description Logics

1 Introduction

Description Logics (DL) have been studied in the past years to provide a formal characterization of frame-based systems. However, while the fragment of first-order logic which char­ acterizes the most popular constructs of these languages has been clearly identified (see for example [Woods & Schmolze, 1992]), there is not yet consensus on the features of frame­ based systems that cannot be formalized in a classical first­ order setting. In fact, frame systems, as well as DL-based systems [Brachman et at., 1990, MacGregor, 1988], ad­ mit forms of nonmonotonic reasoning, such as defaults and closed world reasoning, and procedural features, e.g. rules. These issues have been addressed in the recent literature (see for example [Baader & Hollunder, 1995, Donini et al., 1992, Donini, Nardi, & Rosati, 1995, Padgham & Zhang, 1993, Quantz & Royer, 1992]), but the proposals typically capture one of the above mentioned aspects.

In addition, most implementations of DL-based systems are object-centered, which enables them to perform efficient reasoning on the properties of individuals. Such behaviour can be naturally justified if one can restrict the reasoning to the individuals that are known to the knowledge base (i.e. in­ dividuals that have an explicit name). Based on this intuition, an epistemic extension of DLs with a modal operator K, in­ terpreted in terms of minimal knowledge has been proposed in [Donini et al., 1992]. In that formalism one can express a form of closed-world reasoning, as well as integrity con­ straints in the form of epistemic queries (as proposed in [Re­ iter, 1990]); in addition, by admitting a simple form of epistemic sentences in the knowledge base, one can formalize the so-called procedural rules.

In this paper we propose a new framework of Autoepis­ temic Description Logics (ADLs) which follows the lines of [Donini et al., 1992], extending it in two respects: we rely on the nonmonotonic modal logic MKNF [Lifschitz, 1994] and we consider several kinds of epistemic sentences to be used in the knowledge base. In MKNF one can formalize Default Logic, Autoepistemic Logic, Circumscription and Logic Pro­ gramming, i.e. many of the best known formalisms for non­ monotonic reasoning. With MKNF we can naturally extend the previous approach to modal DLs, by introducing a sec­ ond modal operator interpreted as autoepistemic assumption. Moreover, reasoning methods are available for deduction in propositional MKNF [Rosati, 1997].

As for the representational features of the framework, we show that ADLs are able to capture a large variety of non­ first-order features. In addition to procedural rules and epis­ temic queries, the formalism accounts for defaults, integrity constraints inside the KB, role and concept closure, which are addressed in the paper. Moreover, the whole representational power of MKNF becomes available, thus making it feasible to consider new features, like autoepistemic reasoning, that are not implemented in current DL-based systems.

As for reasoning in ADLs we define methods for query an­ swering which provide sound and complete reasoning proce­ dures in DL-based systems admitting the above mentioned non-first-order features. It turns out that the proposed de­ duction methods constitute interesting decidable extensions of propositional nonmonotonic reasoning.

Based on the above considerations we argue that ADLs can indeed be considered as a unified framework for the logical reconstruction of frame-based systems.

The paper is organized as follows. We first present the ex­ tension of DLs obtained by adding the epistemic operators of MKNF. We then discuss the representational features of ADLs by considering several forms of nonmonotonic reason­ ing and integrity constraints. Finally, we address reasoning in these logics by providing reasoning methods for two rather general cases.

2 Autoepistemic Description Logics

Autoepistemic Description Logics (ADLs) are defined as an extension of DLs, in which the modal operators K and A

are allowed in the formation of concept and role expressions. The meaning of modal sentences is given according to the logic MKNF [Lifschitz, 1994, Lin & Shoham, 1992].

Let VC be a generic description logic. Then, VCK.NF stands for the description logic V C augmented with the modal operators K and A. We say that G is a VCK.NF­ concept if G is a concept expression of VCK.NF· Anal­ ogously, R is a VCK.N:r--role if R is a role expression in Vt:X.NF·

Below we present the epistemic DL ACCK.NF· namely we refer to the DL ACC, although some of the results concern more expressive DLs. The syntax of ACCK.NF is as follows:

where Ga denotes an atomic concept, G (possibly with a sub­ script) denotes a concept, P denotes an atomic role, arid R (possibly with a subscript) denotes a role.

The semantics is obtained by interpreting concepts and roles on MKNF structures. With respect to the original semantics for MKNF in the first-order case, we introduce two changes: (i) foilowing the approach of (Reiter, 1990, Donini et at., 1992] the semantics of ADLs is based on the Rigid Term Assumption: for every interpretation the mapping from the individuals into the domain elements is fixed; (ii) the semantics of ADLs is also based on the following Common Domain Assumption: in each model, every interpretation is defined over the same, fixed, countable-infinite domain of in­ dividuals ~. Hence, we define an epistemic interpretation as a triple (I, M, N) where I is a 'DC-interpretation (a possible world) and M, N are sets of interpretations defined over the domain~.

Atomic concepts and roles are interpreted as subsets of ~ and ~ x ~. respectively. T is interpreted as ~ and ..l as 0. Non-epistemic concepts and roles are given the standard semantics of DLs; conversely epistemic sentences are inter­ preted on epistemic interpretations, as follows.

For example, an individual d E ~ is an instance of a concept KG (i.e. dE (KG)I,M,./11) iff dE G.:l,M,./11 for all interpre­ tations .J E M. In other words, an individual is "known" to be an instance of a concept if it belongs to the concept inter­ pretation of every possible world in M. An individual d E ~ is an instance of a concept AG (i .e. d E (AGf ·M,./11) iff d E G.:l,M,./11 for all interpretations .J E N . In other words, an individual is "assumed" to be an instance of a concept G if it belongs to G in all possible worlds of N. Similarly, an individual d E ~ is an instance of a concept 3KR. T iff there is an individual d 1 E ~ such that (d, d 1 ) E R.:T,M,./11 for all .JE M.

The truth of inclusion statements in an epistemic interpre­ tation (I, M, N) is defined in terms of set inclusion: G ~ D is satisfied in (I, M,N) iff (Gf·M,./11 ~ (Df·M,.N. As­ sertions are interpreted in terms of set membership: G(a) is satisfied in (I, M,N) iff a E (G)I ,M,./11 and R(a, b) is satisfied in (I, M,N) iff (a, b) E (R)I,M,./11. A VCK.N:r-­ knowledge base IJ! is defined as a pair IJ! = (T, A), where T (called TBox) is a finite set of inclusion statements (in­ tensional knowledge) of the form G ~ D, where G, D are VCK.NF-concepts, and A (called the ABox) is a finite set of membership assertions (extensional knowledge) of the form G(a) or R(a, b), where G is a VCK.N:r--concept, R is a VCK.N:r--role, and a, bare individuals in~. We call OE the set of individuals occurring in 1:.

An inclusion G ~ D is satisfied by a structure (M,N) (denoted by (M , N) F IJ!) iff each interpretation I E M is such that (I,M,N) satisfies G ~ D. An asser­ tion G(a) (resp. R(a, b)) is satisfied by (M,N) (denoted by (M,N) F IJ!) iff each interpretation I E M is such that (I, M,N) satisfies G(a) (resp. R(a, b)). A VCXNF~ knowledge base IJ! is satisfied by a structure ( M, N) (de­ noted by (M,N) F IJ!) iff each interpretation I E M is such that every sentence (inclusion or membership assertion) of IJ! is true in the epistemic interpretation (I, M, N).

A set of interpretations M is a model for IJ! iff the structure ( M, M) satisfies IJ! and, for each set of interpretations M 1 , if M c M 1 then ( M 1 , M) does not satisfy IJ! . Roughly speak­ ing, such a preference semantics gives a minimal knowledge interpretation to the modality K, while the operator A is interpreted in terms of autoepistemic assumption (see [Lif­ schitz, 1994, Lin & Shoham, 1992] for further details).

The VCK.NF-knowledge base IJ! is satisfiable if there ex­ ists a model for IJ!, unsatisfiable otherwise. IJ! logically implies an inclusion assertion G ~ D (where G, D are VCK.N:r--concepts), written IJ! F G ~ D, if G ~ D is true in every model for 1J!. Analogously, instance checking in 1: of a membership assertion G(a) (where G is a VCK.N:r-­ concept and a E OE) is defined as follows: IJ! F G(a) iff G (a) is satisfied by every model of IJ! .

3 Reconstruction of frame-based systems

In this section we show that the expressive capabilities of ADLs allow for the reconstruction of several nonmonotonic features of KR systems. In particular, we focus on: defaults, integrity constraints, role and concept closure.

Defaults. Some studies on formalizing defaults in frame­ based systems in DLs [Baader & Hollunder, 1995, Quantz & Royer, 1992] propose the extension of DLs through the use of Default Logic. We argue that, in order to provide a unified framework to the formalization of several forms of KB closure, it is more convenient to treat defaults as epis­ temic sentences. A first attempt in this direction is presented in [Donini, Nardi, & Rosati, 1995], where it is shown that one can translate defaults in a logic of minimal knowledge, but based on a different (and less intuitive) semantics for the modal operator K. In the following, we only address the "closed" semantics for defaults, but it is worth noticing that also different forms of "open" semantics (see e.g. [Kamin­ ski, 1995]) can be formalized in ADLs. We call V .C-default a default rule of the form d = a:(3, , ... ,(3n , where a, f3i , 'Y are 'Y V.C-concepts and n ~ 0.

The semantics proposed in [Baader & Hollunder, 1995] for defaults in V.C-KBs restricts the application of defaults only to the individuals explicitly mentioned in the ABox. Notice that this semantics can be viewed as the natural extension of the semantics of procedural rules given in [Donini et al., 1992], where rules are applied only to the known individu­ als in the KB. Under this assumption, we are able to translate default rules in terms of V.CKN:F inclusions in the frame­ work of ADLs. To this purpose, the translation of defaults into MKNF [Lifschitz, 1994] provides a modular and faithful translation of default rules into V.CKN:F· More specifically, a V.C-default dis translated as:

where I is an atomic concept not appearing in the KB.

Let (E, V ) be a pair such that E = (T, A) is a V.C-KB and Vis a set ofV.C-defaults. Then, TnK(E, V) = (T', A 1 ), where T' = T U {TnK(d) : d E V}, A 1 = AU {I(a) : a E OE}, i.e. for each individual a E 0~;, the assertion I(a) is added to A . The condition KI corresponds to adding an extra prerequisite for the application of the default, which ex­ presses the fact that the individual must be in OE. Such an extra condition is needed to realize the closed semantics for prerequisite-free defaults. Indeed, without imposing the pre­ requisite I, a prerequisite-free default would be applicable to each individual of 6. The resulting modular translation based on TDK is faithful.

Theorem 3.1 Given a V.C-KB with defaults (E, V), where E is a V.C-KB and Vis a set ofV.C-defaults, the V.CKN:F KB TDK(E , V) is such that (E, D) I= C(a) iff TnK(E , V) I= C(a) for each V.C-concept C and each a E Or; .

Integrity Constraints. In this section we study the prob­ lem of representing integrity constraints (IC) in ADLs. [Re­ iter, 1990] pointed out the epistemic nature of ICs : they are not statements about the world, they are statement about what the KB is said to know. Generally speaking, the satisfaction of ICs in Reiter's approach is checked in the following way: let P be a property that the KB must satisfy. Find a suitable epistemic query Qp formalizing P. Then, check whether the KB (interpreted under a closure assumption) entails Qp.

Previous work [Donini et al., 1992] has shown that Reiter's approach can be realized in V.C-KBs by endowing the query language with epistemic abilities. Nevertheless, it would be very desirable to express ICs as any other piece of informa­ tion on the domain of interest, i.e. as sentences inside the KB. The difficulty that arises is precisely in the formaliza­ tion of the notions of closure underlying these forms of in­ tegrity constraints. Notably, ICs do not add "objective infor­ mation": rather, they impose conditions on the consistency of the KB. This is true in the case of first-order KBs, or KBs with a single model as in the case under consideration. In the case of KBs with multiple models, ICs can be viewed as an a fortiori check which establishes which of the models are actually allowed. In particular, many forms of ICs impose properties that must hold for the known individuals of the KB. The modal operator K appears as an appropriate way to for­ malize this intuition. Moreover, conditions imposed by ICs are consistency conditions which cannot change the content of the KB. In other words, augmenting the KB with ICs can only have one of the following two possible effects: either the model of the KB remains unchanged (it satisfies the ICs), or the KB becomes inconsistent (since its model does not satisfy the ICs). As we shall see, the modal operator A turns out to be well-suited to this purpose.

We now show that the combination of the modalities K and A provides for the formalization in ADLs of sophisticated constraints on the KB content.

Example 1. Let us consider the IC "each known person must be known to be either male or female", which is meant to avoid any situation where an individual has been added to the KB without specifying her/his sex. One might attempt to for­ malize it through the V.CKN:F inclusion h = Kperson ~ (Kmale U Kfemale) . However, this formalization is incor­ rect, since such an assertion forces in the KB the knowledge about the sex of each known person. Instead, the meaning of the IC is to check whether the sex of each known per­ son is known to the KB. This difference can be better ex­ plained as follows . Suppose E contains only one assertion, person(Bob). Of course, E does not satisfy the IC. Now, if we add I 1 toE, we obtain two models for (E, {II}): one in which male(Bob) holds, and another in which female(Bob) holds. On the contrary, we would like (E, { I 1}) to be in­ consistent, since E does not satisfy the IC. The solution to the above problem lies in the use of the autoepistemic belief operator A . Indeed, if we add to a KB the V.CKN:F inclu­ sion If = Kperson ~ (Amale U Afemale) we formalize the intended meaning of the IC. The difference between h and Ii lies in the fact that If does not force any new knowl­ edge on known persons. In our example, since person(Bob) holds, the assertion Amale U Afemale(Bob) must hold. Now, since there is no reason to conclude either male(Bob) or female(Bob) from E, the autoepistemic beliefs Amale(Bob) and Afemale(Bob) are not consistent with the objective knowledge of E, therefore Amale U Afemale(Bob) is in­ consistent with E . 0

We remark that there is a precise correspondence between the A operator and Moore's L operator of Autoepistemic Logic [Rosati, 1997]. From this correspondence, the above example can also be understood as a variation of the "classi­ cal" inconsistent autoepistemic theory { Lcp} . Thus, the idea in the formalization of ICs is precisely to represent an IC as a believed sentence: if such a belief is not "supported" by the objective knowledge, then an inconsistency arises.

Example 2. The IC "Each known employee must have a known social security number, which must be known to be valid" can be correctly formalized by the set of ACCKNF assertions l2 = {-.Kemp U 3KSSN.A valid( a) I a E OE}. In fact, it can be shown that an ACCKNF ABox does not satisfy the IC iff E U ! 2 is inconsistent. 0

Role and concept closure. Finally, we show how two par­ ticular forms of closed-world reasoning, namely role closure and concept closure, can be nicely formalized in the frame­ work of V CKN F. These kinds of closure appear as very use­ ful tools in knowledge representation.

Closure on roles is available both in CLASSIC [Brachman et al., 1990] and in LOOM [MacGregor, 1988]. The idea is to restrict universal role quantifications to the known individuals filling the role in the KB.

Example (Role closure). Let \[1 1 be the following ACC-KB: {CHILD( Ann, Marc), CHILD( Ann, Paula)}, where doctor is an abbreviation for the concept dn-.lnrich, and lawyer is an abbreviation for lnrich (expressing that doctors and lawyers are disjoint concepts, and both are rich). Now, suppose we want to formalize the property: "one of the known children of Ann is known to be a doctor, and another one. is known to be a lawyer". One would like to conclude that "all known children of Ann are known to be rich". It turns out that the correct formalization is pro­ vided by the use of both modalities A and K. Formally: let B = 3ACHILD.Kdoctor n 3ACHILD.Klawyer(Ann). Then, \[1 1 U {B} I= 'v'KCHILD.Krich(Ann). 0

Epistemic operators make it natural to extend the notion of closure to concept expressions.

Example (Concept closure). Let W2 be the following ACCK-KB: { doctor(Paula), lawyer(Marc), 'VCHILD.hasBlueEyes(Ann)}. Suppose we want to add to \[12 the following informal property P: "One of Ann's children is one of the known doctors". Now, since Paula is the only known doctor, we want to be able to conclude that Paula is one of Ann's children, and hence \[1 2 U {P} I= hasBlueEyes(Paula). This can be obtained by formaliz­ ing P through the assertion 3KCHILD.Adoctor(Ann), since it can be shown that all models for the KB \[12 U {P} ei­ ther Paula or Marc is one of Ann's children. Therefore, Wz U {P} I= hasBlueEyes(Paula) . 0

4 Reasoning in ADLs

In this section we study reasoning in ADLs. First, we study VCKNrsimple KBs, i.e. VCKNF-knowledge bases in which there is no occurrence of epistemic operators in the scope of quantifiers. We prove that decidability is preserved in simple theories. Furthermore, in many cases the worst-case complexity of deduction is not affected by such a nonmono­ tonic extension. We also provide an algorithm for instance checking in V CKN F-simple KBs which is parametric wrt the DL in which the KB is expressed. As we shall see, such an algorithm allows for reasoning in DLs with (closed) defaults.

Then, we address subjectively quantified ACCKNr ABoxes, i.e. ACCKNF-ABoxes in which occurrences of epistemic operators in the scope of quantifiers are allowed (under some restrictions). We prove that instance checking in such ABoxes is decidable. This result allows us to prove decidability of reasoning in DLs with features like role and concept closure and integrity constraints, which can be ex­ pressed in ACCKNrABoxes with quantifying-in, as shown in the previous section.

Notably, in the case of ACCKNF we can easily reduce a simple KB to a subjectively quantified ABox. On the other hand, the method for reasoning on simple KBs is applica­ ble to any non-modal DL for which a procedure for instance checking is available.

4.1 Reasoning without quantifying-in

We start by defining the notion ofVCKNrsimple KBs.

Definition 4.1 A VCKNF-concept C is simple iff there are no occurrences in C of an epistemic operator in the scope of quantifiers.

Definition 4.2 A VCKNrsimple KB is a pair (E, f) such that E = (T, A) is a VC-KB and r is a set of VCKNF­ simple inclusions, i.e. inclusions of the form KG I; D, where Dis a VCKNrsimple concept and Cis a VC-concept such that E ~ T I; C.

As in [Donini et al., 1992], the conditionE ~ T I; C cor­ responds to a "closed" semantics for the VCKNF-simple in­ clusion KG I; D, in the sense that it corresponds to consider the application of such axioms only to the individuals in Or; . This is precisely due to the minimal knowledge semantics of the modal operator K: in fact, due to the form of VCKNF­ simple inclusions, there is no way to force the property KG on individuals tJ. Or; (since E ~ T I; C). Now, from the definition of model in VCKNF (that is, from the minimal knowledge semantics of the operator K) it is easy to see that only sets of V £-interpretations in which -.KG holds for each individual not in Or; are preferred. That is, the application on such individuals of the epistemic inclusion KC I; D has no effect. Therefore, the following property holds.

Lemma4.3 LetE = ((T,A),r) beaVCKNF-simpleKB. Let E' = (T U r,A), and let E" = (T,A U {·KC u D(a)IKC I; DE rand a E OE}). Then, the sets of models ofE' and E" coincide.

We now present a method for computing instance check­ ing in VCKNF-simple KBs, based on the procedure defined for propositional MKNF theories (see [Rosati, 1997]). How­ ever, the extension to the case of ADLs requires several pre­ liminary notions. In particular, we have to define consistency of a partition of assertions wrt a VCKNrsimple KB.

Definition 4.4 Let C be a VCKNF-concept expression. Let P, N be sets of VCKNF-assertions of the form KD(a), AD(a), such that P n N = 0. Then, C(a)(P, N) is the assertion obtained by substituting with T each occur­ rence in C of a concept D which is not within the scope of a modal operator, and such that D(a) E P, and with .leach occurrence in C of a concept D which is not within the scope of a modal operator, and such that D(a) E N .

Informally, G(a)(P, N) is the assertion representing the eval­ uation of G(a) wrt the guess of the modal subformulas of G(a) according to the partition (P, N) . Notice that, if each modal subexpression in G(a) appears either in P or in N, then G(a)(P, N) is a non-modal assertion. We denote pK = {G(a)(P,N)IKG E Panda E OE}, pA = {G(a)(P, N»AG E Panda E OE}, and APK = {AG(a)IG(a) E P }.

In order to reason with V.CK...v.r-simple KB we need an ef­ fective method for identifying models. Let G be a V.CK...v;::­ concept. The set of modal atoms of G, denoted as M A( G), is the set of role subexpressions or concept subexpressions of G of the form KG' or AG'. The set of modal atoms of an in­ clusion G ~Dis the union of the sets M A( G) and M A( D).

Definition 4.5 Let 'Y be a V.CK...v;::-inclusion. Let 0 be a set of individuals. Let M A(r) be the set of modal atoms in 'Y· Then, the set of instances of M A(r) in 0, denoted as M I(/ , 0), is the set {G(a)la E 0 and G E M A(r )}. More­ over, ijf is a set ofV.CK...v.r-inclusions, then M A(r, 0) = U-rEf M A( 'Y' 0).

Definition 4.6 Let (1;, r) be a V.CK...v.r-simple KB. Let (P, N) be a partition of M I(r, OE). Then, (P, N) is con­ sistent with (1;, r) iff the following conditions hold: i.foreachr E fandforeacha E OE, r (a)(P,N) := T; ii. the V.C-knowledge base (T, AU pK) is satisfiable; iii. the V.C-knowledge base (T, AU pA) is satisfiable; iv. for each KG(a) E N, 1; U pK ~ G(a)(P, N); v. for each AG(a) EN, 1; U p A ~ G(a)(P, N).

Notice that in the above definition both pK and pA are sets of V £-assertions, since ( P, N) is a partition of M I (r, OE). Therefore, (T, AU pK) and (T, AU pA) are V.C-KBs .

Lemma 4.7 Let (P, N) be defined as above. (P, N) identi­ fies a model for (T u r , A) iff

i. (P, N) is consistent with (1;, r);

ii. 1; U pK F pA;

iii. for each partition (P', N') of M I(f', OE), where r' = r u { APK} either (a) (P', N') is not consistent with (1;, r) or (b) 1; U pK ~ P'K or (c) 1; U P'K f= pK or (d) l;UPK ~ptA .

The proof follows from Lemma 4.3 and properties of the logic MKNF [Rosati, 1997]. Based on the above lemma, we can provide a procedure for estabilishing whether a partition (P, N) identifies a model for (T U r, A).

Figure 1 reports the algorithm Simple-Not-Entails for com­ puting instance checking in V.CK...v;::-simple KBs. Notice that, in the case when the query G(a) is non-modal, the method can be realized using a procedure for computing in­ stance checking in V.C.

Based on the algorithm Simple-Not-Entails, one can prove decidability of instance checking in V.CK...v;::-simple KBs.

Theorem 4.8 Let (1;, r) be a V.CK...v.r-simple KB. Let G(a) be a V.C-assertion. The problem (1;, f) f= G(a) is decidable iff instance checking in V .C is decidable.

We can provide a computational characterization of the in­ stance checking problem in V.CK...v;::-simple KBs. In par­ ticular, the above theorem implies that adding A.CCK...v;::­ simple inclusions to an A.CC-KB with empty TBox 1; =

(0, A) does not increase the worst-case complexity of in­ stance checking of an A.CCK-assertion, which is PSPACE­ complete in the case of a non-modall; [Donini et al., 1992]. The same result holds in the case of an A.CC-KB 1; = (T, A) with A.CCK...v;::-simple inclusions (i .e. instance checking is EXPTIME-complete as in the non-modal case).

Notably, it is easy to see that the translation TDK (1;, V) of a V.C-KB with defaults (1;,V) is equivalent to the V.CK...v.r­ simple KB (1;, f), in which f is the set { TDK(d) : d E V} . Therefore, from Theorem 3.1 it follows that in many cases adding defaults to a V .C-KB does not increase the complexity of deduction: in particular, reasoning in A.CC-ABoxes with defaults is PSPACE-complete.

4.2 Reasoning with quantifying-in

We start by defining the notion of subjectively quantified A.CCK...v.r-ABoxes.

Definition 4.9 A subjectively quantified A.CCK...v.r-assertion is an A.CCK...v;::-assertion G(a) where G is a concept expres­ sion of A.CCK...v;:: in which each quantified subexpression is oftheform 3P.D', VP.D', 3MP.M'D, VMP.M'D, where M, M' E {K, A}, D' is an A.CC-concept, Pis an atomic role.

An A.CCK...v;::-ABox composed of subjectively quantified assertions is called subjectively quantified A.CCK...v;::-ABox. The method for reasoning on subjectively quantified ABoxes is based on a tableaux calculus following the lines of [Donini et al., 1996], where special closure conditions are defined to enforce the preference criterion on the models represented by the branches of the tableau. For ADLs, the lifting from propositional logic to DLs raises several difficulties that are addressed in the sequel. In particular, we sketch a calcu­ lus for characterizing the models of a subjectively quantified A.CCK...v;::-ABox in terms of A.CC-KBs, to which the proce­ dure for query answering defined in [Donini et al., 1992] can be applied.

The tableaux rules include the standard rules for an 55 tableau [Fitting, 1983] for handling propositional connec­ tives and epistemic expressions of the form KG, AG and -.KG, -.AG. The tableaux calculus for generating the mod­ els for subjectively quantified A.CC-KBs behaves as usual, except for the fact that each rule is applied only to epistemic prefixed formulas.

First, we define the notion of modal atoms of a subjec­ tively quantified A£CKN.r-assertion C(x) as the set of as­ sertions C'(x), where C' is a subexpression of C of the form KG" or AC" or 3MP.M' C" or 'v'MP.M' C", where M, M' E {K, A}. The set of modal atoms M A(~) of a sub­ jectively quantified A£CKN.r-ABox ~ is the union of the sets of modal atoms of all the assertions it contains.

A branch B is a set of prefixed formulas of the form (w : C(x)). The tableau for ~ starts with the set { (1 : KA) I assertion A E ~}. Oa is the set of individuals in B.

We concentrate on the rules that handle subjectively quan­ tified expressions, and on a rule that saturates the branch wrt modal atoms of~- We phrase them using K; the cases arising from the use of both modalities K and A are analogous. The rules are as follows :

'v'-rule: if (w : 'v'KP.KC(x)) E B, then for each (1 : KP(x, y)) E B add (1 : KC(y)) to B.

3-rule: if (w : 3KP.KC(x)) E Band there is no y such that both (1 : KP(x,y)) and (1 : KC(y)) E B, then add (1 : KP(x, z)) and (1 : KC(z)) to B, where z E Oau{~}and~rf.Oa.

mcut-rule: if KC(x) E M A(~) then add (1 : KC(x)) or (1 : -,KC(x)) to B, if neither is present in B.

A branch is completed if no rule is applicable to it; a branch is open if there is no pair of prefixed formulas in B of the form (w: C(x)) and (w: -,C(x)) .

An open completed branch B does not always represent a model. To select models according to the preference criterion, one needs to characterize the objective knowledge associated with B. In particular, one has to distinguish between the objective knowledge implied by K-prefixed and A-prefixed modal atoms [Rosati, 1997]. To this aim, we remark that the mcut-rule forces a partition on the modal atoms of ~ in B. We call (Pa, Na) such a partition. Based on Def. 4.4, we define the following A£C-ABoxes:

We can now define the notion of preferred branch.

Definition 4.10 A branch B of the tableau for~ is preferred iff B is open and completed, OBJ x(B) f= OBJ A(B) and, for each open and completed branch B' of the tableau for E u {AC(x)IC(x) E OBJ x(B)}, either OBJ x(B) ~ OBJ x(B') or OBJ x(B') f= OBJ x(B) or OBJ x(B) ~ OBJ A(B').

The above notion of preferred branch allows us to identify all the models of~. up to renaming of individuals in Oa-Or;.

Theorem 4.11 Let~ be a subjectively quantified A£CKN.r­ ABox. Then, a branch B of the tableau for ~ is preferred iff there exists a model Mfor ~and a mapping fL : D. --+ D. such that M = {III f= J.L( OBJ x(B))}. Moreover, letC(a) bean A£CK-assertion. Then, ~ f= C(a) iff there exists a preferred branch B of the tableau for~ such that OBJ x(B) ~ C(a).

It can be shown that the tableaux method above outlined al­ ways terminates. Moreover, since OBJ x(B) ~ C(a) can be checked by the algorithm presented in [Donini et al., 1992], we have proved decidability of the instance checking problem for subjectively quantified A£CKN.r-ABoxes.

Acknowledgments

This research has been funded by Italian MURST, "Tecniche di ragionamento non monotono" and "Linguaggi per la mod­ ellizzazione concettuale dei requlsiti", by EC Esprit LTR Project "Foundations of Data Warehouse Quality", and by ASI (Italian Space Agency).