Introduction

Description logics (DLs) [1] are central to many modern AI and database applications since they provide the logical foundation of formal ontologies. Yet, as classical formalisms, DLs do not allow for the proper representation of and reasoning with defeasible information, as shown up in the following example from the access-control domain: employees have access to classified information; interns (who are also employees) do not; but graduate interns do. From a naïve (classical) formalisation of this scenario, one concludes that the class of interns is empty (just as that of graduate interns). But while concept unsatisfiability has been investigated extensively in ontology debugging and repair, our research problem here goes beyond that.

The past 25 years have witnessed many attempts to introduce defeasible-reasoning capabilities in a DL setting, usually drawing on a well-established body of research on non-monotonic reasoning (NMR). These comprise the so-called preferential approaches [13-15, 23, 24, 22, 26, 27, 29, 30, 38, 39], circumscription-based ones [6,7,40], as well as others [2, 3, 5, 25, 31-33, 36, 37, 42].

Preferential extensions of DLs turn out to be particularly promising. There a notion of defeasible subsumption ∼ is introduced, the intuition of a statement of the form C ∼ D being that "usually, C is subsumed by D" or "the normal Cs are Ds". The semantics is in terms of an ordering on the set of objects allowing us to identify the most normal elements in C with the minimal C-instances w.r.t. the ordering.

The assumption of a single ordering on the domain of interpretation does not allow for different, possibly incompatible, notions of defeasibility in subsumption resulting from the fact that a given object may be more exceptional than another in some context but less exceptional in another. Defeasibility therefore introduces a new facet of contextual reasoning not present in deductive reasoning. In recent work [21] we addressed this limitation by allowing different orderings on objects, using preference relations on role interpretations [17]. Here we complete the picture by also providing a proof-theoretic counterpart and associated results.

After setting up the notation and our access-control example in Section 2, we give a summary of our context-based defeasible DL (Section 3). In Section 4, we define a tableau-based algorithm for checking consistency of contextual defeasible knowledge bases. The paper concludes with a discussion on future directions of investigation.

Notation and an example

We assume finite and pairwise disjoint sets C, R and I standing for, respectively, concept, role and individual names. With A, B, . . . we denote concept names, with r, s, . . ., role names, and with a, b, . . ., individual names. In the access-control scenario above we could have, for example, C = {Classified, Employee, Graduate, Intern, ResAssoc}, R = {hasAcc, hasJob, hasQua}, and I = {anne, bill, chris, doc123}, with the respective obvious intuitions. Complex concepts are denoted C, D, . . . Figure 1 depicts an interpretation for our access-control example with domain ∆ I = {x i | 0 ≤ i ≤ 11}, and interpreting the elements of the vocabulary as follows: Classified I = {x 10 }, Employee I = {x 0 , x 4 , x 5 , x 9 }, Graduate I = {x 4 , x 5 , x 6 , x 9 }, Intern I = {x 0 , x 4 }, ResAssoc I = {x 5 , x 6 , x 7 }, hasAcc I = {(x 4 , x 10 ), (x 9 , x 10 ), (x 6 , x 10 ), (x 6 , x 11 )}, hasJob I = {(x 0 , x 3 ), (x 4 , x 3 ), (x 9 , x 3 ), (x 5 , x 1 ), (x 6 , x 1 )}, and hasQua I = {(x 4 , x 8 ), (x 9 , x 8 ), (x 5 , x 2 ), (x 6 , x 2 ), (x 7 , x 2 )}. Further, anne I = x 5 , bill I = x 0 , chris I = x 6 , and doc123 I = x 10 .

The knowledge base KB = T ∪ A, with T and A as below, is a first stab at formalising our access-control example:

T =                        Intern Employee, Employee ∃hasJob. , Graduate hasQua. , Employee ∃hasAcc.Classified, Intern ¬∃hasAcc.Classified, Intern Graduate ∃hasAcc.Classified, ResAssoc ¬Employee, ResAssoc Graduate                        A =        anne : ResAssoc, chris : ResAssoc, doc123 : Classified, (chris, doc123) : hasAcc       

It is not hard to see that this knowledge base is satisfiable and to check that KB |= Intern ⊥. Incoherence of the knowledge base is but one of the (many) reasons to go defeasible. Armed with a notion of defeasible subsumption of the form C ∼ D [15], of which the intuition is "normally, C is subsumed by D", formalised by the adoption of a preferential semantics à la Shoham [41], we can give a more refined formalisation of our scenario example with KB = T ∪ D ∪ A, where T and D are given below (D standing for a defeasible TBox) and A is as above:

T =    Intern Employee, Employee ∃hasJob. , Graduate hasQua.    D =            Employee ∼ ∃hasAcc.Classified, Intern ∼ ¬∃hasAcc.Classified, Intern Graduate ∼ ∃hasAcc.Classified, ResAssoc ∼ ¬Employee, ResAssoc ∼ Graduate           

Then, one could ask whether intern research associates are usually graduates, and whether they should usually have access to classified information. It soon becomes clear that modelling defeasible information is more challenging than modelling classical information, and that it becomes problematic when defeasible information relating to different contexts are not modelled independently.

Suppose, for example, that Chris is a graduate research associate who is also an employee, and Anne is a research associate who is neither a graduate nor an employee. In any preferential model of the defeasible KB, both Chris and Anne are exceptional in the class of research associates. This follows because Chris is an exceptional research associate w.r.t. employment status, and Anne is an exceptional research associate w.r.t. qualification. Also, in any preferential model of KB Chris and Anne are either incomparable, or one of them is more normal than the other. Since context has not been taken into account, there is no model in which Anne is more normal than Chris w.r.t. employment, but Chris is more normal than Anne w.r.t. qualification.

Contextual defeasible ALC

Contextual defeasible ALC (dALC) smoothly combines in a single logical framework the following features: all classical ALC constructs; defeasible value and existential restrictions [12,17]; defeasible concept inclusions [15], and context [18,21].

Let C, R and I be as before. Complex dALC concepts are denoted C, D, . . ., and are built according to the rules:

C ::= | ⊥ | C | (¬C) | (C C) | (C C) | (∃r.C) | (∀r.C) | ( − ∼ − | r.C) | ( ∼ r.C)

With L dALC we denote the language of all dALC concepts (including all ALC concepts). Again, when writing down elements of L dALC , we shall omit parentheses whenever they are not necessary for disambiguation. An example of dALC concept is ResAssoc ( ∼ hasAcc.¬Classified) (∃hasAcc.Classified), denoting those research associates whose normal access is only to non-classified info but who also turn out to have some (exceptional) access to a classified document.

The semantics of dALC is anchored in the well-known preferential approach to non-monotonic reasoning [34,35,41] and its extensions [8-11, 16, 19, 20], especially those in DLs [15,17,28,38,43].

Let X be a set. With #X we denote the cardinality of X. A binary relation is a strict partial order if it is irreflexive and transitive. If < is a strict partial order on X, with

min < X = def {x ∈ X | there is no y ∈ X s.t. y < x} we denote the minimal elements of X w.r.t. <. A strict partial order on a set X is well-founded if for every ∅ = X ⊆ X, min < X = ∅. Definition 1 (Ordered interpretation). An ordered interpretation is a tuple O = def ∆ O , • O , O such that: -∆ O , • O is an ALC interpretation, with A O ⊆ ∆ O , for each A ∈ C, r O ⊆ ∆ O × ∆ O

, for each r ∈ R, and a O ∈ ∆ O , for each a ∈ I, and

-O = def O r1 , . . . , O r #R , where O ri ⊆ r O i × r O i , for i = 1, . . . , #

R, and such that each O

ri is a well-founded strict partial order.

Given O = ∆ O , • O , O

, the intuition of ∆ O and • O is the same as in a standard ALC interpretation. The intuition underlying each of the orderings in O is that they play the role of preference relations (or normality orderings), in a sense similar to the preference orders introduced by Shoham [41] in a propositional setting, and investigated by Kraus et al. [34,35] and others [9-11, 13, 26]: The pairs (x, y) that are lower down in the ordering O ri are deemed as most normal (or typical, or expected, or conventional) in the context of (the interpretation of) r i .

O hasAcc = {(x 6 x 11 , x 6 x 10 )}, O hasJob = {(x 9 x 3 , x 0 x 3 ), (x 0 x 3 , x 4

x 3 ), (x 9 x 3 , x 4 x 3 ), (x 0 x 3 , x 5 x 1 ), (x 9 x 3 , x 5 x 1 ), (x 6 x 1 , x 5 x 1 )}, and O hasQua = {(x 5 x 2 , x 6 x 2 ), (x 6 x 2 , x 7 x 2 ), (x 5 x 2 , x 7 x 2 )}. (For the sake of readability, we shall henceforth sometimes write rtuples of the form (x, y) as xy.)

In the following definition we extend ordered interpretations to complex concepts of the language. to {x}). The interpretation function • O interprets dALC concepts as follows:

Definition 2 (Interpretation of concepts). LetO = ∆ O , • O , O , let r ∈ R and, for each x ∈ ∆ O , let r O|x = def r O ∩ ({x} × ∆ O ) (i.e., the restriction of the domain of r O ∆ O Class O Emp O Grad O Int O RA O x0(b) x1 x2 x3 x4 x5(O = def ∆ O ; ⊥ O = def ∅; (¬C) O = def ∆ O \ C O ; (C D) O = def C O ∩ D O ; (C D) O = def C O ∪ D O ; (∃r.C) O = def {x ∈ ∆ O | r O (x) ∩ C O = ∅}; (∀r.C) O = def {x ∈ ∆ O | r O (x) ⊆ C O }; ( − ∼ − | r.C) O = def {x ∈ ∆ O | min O r (r O|x )(x) ∩ C O = ∅}; ( ∼ r.C) O = def {x ∈ ∆ O | min O r (r O|x )(x) ⊆ C O }.

Analogously to the classical case, ∼ and − ∼ − | are dual to each other. As an example, in the ordered interpretation O of Figure 2, we have that

( − ∼ − | hasAcc.Classified) O = ∅ = (¬ ∼ hasAcc.¬Classified) O , whereas (∃hasAcc.Classified) O = {x 6 }.

Defeasible ALC also adds contextual defeasible subsumption statements to knowledge bases. Given C, D ∈ L dALC and r ∈ R, a statement of the form C ∼ r D is a (contextual) defeasible concept inclusion (DCI), read "C is usually subsumed by D in the context r". A dALC defeasible TBox D (or dTBox D for short) is a finite set of DCIs. A dALC classical TBox T (or TBox T for short) is a finite set of (classical) subsumption statements C D (i.e., T may contain defeasible concept constructs, but not defeasible concept inclusions). Given T , D and A, with KB = def T ∪ D ∪ A we denote a dALC knowledge base, a.k.a. a defeasible ontology, an example of which is given below:

T =        Intern Employee, Employee ∃hasJob. , Graduate hasQua. , ResAssoc ∼ hasAcc.¬Classified        A =                anne : Employee, anne : ResAssoc, bill : Intern, chris : ResAssoc, doc123 : Classified, (chris, doc123) : hasAcc                D =            Employee ∼ hasJob ∃hasAcc.Classified, Intern ∼ hasJob ¬∃hasAcc.Classified, Intern Graduate ∼ hasJob ∃hasAcc.Classified, ResAssoc ∼ hasJob ¬Employee, ResAssoc ∼ hasQua Graduate            Definition 3 (Satisfaction). Let O = ∆ O , • O , O , r ∈ R, C, D ∈ L dALC , and a, b ∈ I. Define ≺ O r ⊆ ∆ O × ∆ O as follows: ≺ O r = def {(x, y) | there is (x, z) ∈ r O s.t. for all (y, v) ∈ r O , ((x, z), (y, v)) ∈ O r }.

The satisfaction relation is defined as follows:

O C D if C O ⊆ D O ; O C ∼ r D if min ≺ O r C O ⊆ D O ; O a : C if a O ∈ C O ; O (a, b) : r if (a O , b O ) ∈ r O . If O α,(resp. r ∈ R) is satisfiable w.r.t. KB if there is a model O of KB s.t. C O = ∅ (resp. r O = ∅).

One can check that the interpretation O in Figure 2 satisfies the above knowledge base. To help in seeing why, Figure 3 depicts the contextual orderings on objects (represented with dotted arrows) induced from those on roles in O as specified in Definition 3. It follows from Definition 3 that, if O r = ∅, i.e., if no r-tuple is preferred to another, then ∼ r reverts to a context-agnostic classical . A similar observation holds for individual concept inclusions: if (C ∃r. ) O = ∅, then C ∼ r D reverts to C D. This reflects the intuition that the context r is taken into account through the preference order on r O . In the absence of any preference, the context becomes irrelevant. This also shows why the classical counterpart of ∼ r is independent of r -context is taken into account in the form of a preference order, but preference has no bearing on the semantics of .

∆ O Class O Emp O Grad O Int O RA O x0(b) x1 x2 x3 x4 x5(

Contextual defeasible subsumption ∼ r can also be viewed as defeasible subsumption based on a preference order on objects in the domain of r O obtained from O r . Non-contextual defeasible subsumption can then be obtained as a special case by introducing a new role name r and axiom ∃r. . Given a dALC knowledge base KB, a fundamental task from the standpoint of knowledge representation and reasoning is that of deciding which statements follow from KB and which do not.

Definition 4 (Preferential entailment).

A statement α is preferentially entailed by a dALC knowledge base KB, written KB |= pref α, if O α for every O s.t. O KB.

The following lemma shows that deciding preferential entailment of GCIs and assertions can be reduced to dALC knowledge base satisfiability, a result that will be used in the definition of a tableau system in Section 4. Its proof is analogous to that of its classical counterpart in the DL literature and we shall omit it here: It turns out that deciding preferential entailment of DCIs too can be reduced to dALC knowledge base satisfiability, but first, we introduce the tableau-based algorithm for deciding preferential consistency.

Tableau for preferential reasoning in dALC

In this section, we define a tableau method for deciding preferential consistency of a dALC knowledge base. Our terminology and presentation follow those of Baader et al. [4] in the classical case.

We start by observing that, for every ordered interpretation O and every

C, D ∈ L dALC , O C D if and only if O ¬C D.

In that respect, we can assume w.l.o.g. that all GCIs in a TBox are of the form E, for some E ∈ L dALC . Note also that we can assume w.l.o.g. that the ABox is not empty, for if it is, one can add to it the trivial assertion a : , for some new individual name a. It is easy to see that the resulting (non-empty) ABox is preferentially equivalent to the original one.

Definition 5 (Subconcepts). Let C ∈ L dALC . The set of subconcepts of C, denoted sub(C), is defined inductively as follows: We are now ready for the definition of the expansion rules for dALC-concepts. They are shown in Figure 4. The -, -, ∀-, and T -rules work as in the classical case [4], whereas the remaining rules handle the additional dALC constructs according to our preferential semantics. We shall explain them in more detail below. Before doing so, we need a few more definitions, in particular of what it means for an individual to be blocked, as tested by the ∃-, − ∼ − | -, and ∼ -rules and needed to ensure termination of the algorithm we shall present.

-If C = A, for A ∈ C ∪ { , ⊥}, then sub(C) = def {A}; -If C = C 1 C 2 or C = C 1 C 2 , then sub(C) = def {C} ∪ sub(C 1 ) ∪ sub(C 2 ); -If C = ¬D or C = ∃r.D or C = ∀r.D or C = − ∼ − | r.D or C = ∼ r.D, then sub(C) = def {C} ∪ sub(D).

As can be seen in the expansion rules, our tableau method makes use of a few auxiliary structures, which are built incrementally during the search for a model of the input knowledge base. The first one is a partial order on pairs of individuals ρ r A , for each r ∈ R. Its purpose is to build the skeleton of an r-preference relation on pairs of individual names appearing in an ABox A. In the unravelling of the complete clashfree ABox (see below), if there is any, ρ r A is used to define a preference relation on the interpretation of role r in the constructed ordered interpretation.

The second auxiliary structure is a pre-order σ r A on individual names, for each r ∈ R. It fits the purpose of keeping track of which individuals are to be seen as more normal (or typical) relative to others in the application of the ∼ -rule (see Figure 4) so that the associated ρ r A -ordering can be completed (by the -rule) and, in the unravelling of the model, deliver an induced ≺ r that is faithful to σ r A . (This point will be made more clearly in the explanation of the relevant rules. In particular, the reason why σ r A is a pre-order and not a partial order like ρ r A will be explained in the soundness proof.) Intuitively, σ r A corresponds to the converse of the preference order introduced in Definition 3.

Finally, the third structure used in the expansion rules is a labelling function τ r A (a) mapping an individual name a to the set of concepts a ought to be a minimal instance of in the context r w.r.t. the ABox A. The purpose of τ r A (a) is threefold: (i) it is needed to ensure the minimal elements of a concept C inherit all defeasible properties encoded in the DCIs (see ∼ -rule); (ii) it flags that every individual more preferred than a should be marked as ¬C, as performed by the min-rule, and (iii) it plays a role in the blocking condition (see below) to prevent the generation of an infinite chain of increasingly more normal elements in σ r A . Note that ρ r A , σ r A and τ r A (a) are only used in the inner workings of the tableau and are not accessible to the user. The following definition is used in the expansion rules of Figure 4 to ensure termination:

Definition 9 (Blocking). Let A be an ABox, a, b ∈ I, and let σ r A and τ r A be as above. We say that b is blocked by a in A in the context r if (1) a is either an r-ancestor or a σ r A -ancestor of b, (2) con A (b) ⊆ con A (a), and (3) τ r A (b) ⊆ τ r A (a). We say b is blocked in A if itself or some r-ancestor or σ r A -ancestor of b is blocked by some individual. The -, -, ∀-, and T -rules in Figure 4 are as in the classical case and need no further explanation.

The − ∼ − | -rule creates a most preferred (relative to individual a) r-link to a new individual falling under concept C. Notice that this is achieved by just adding an assertion (a, d) : r to A, for d new in A, since there shall never be (a, e) with (ae, ad) ∈ ρ r A . The ∼ -rule is analogous to the ∀-rule, but propagates a concept C only to those individuals across preferred r-links (i.e., r-links that are minimal in ρ r A ). The ∃-rule handles the creation of an r-successor without the information whether such an r-link is relatively preferred or not. In this case, both possibilities have to be explored, which is formalised by the or-branching in the rule. In one case, a preferred r-link is created just as in the − ∼ − | -rule; in the other, an r-link is created along with an extra one which is then set as more preferred to it (in ρ r A ). The ∼ -rule handles the presence of DCIs in the knowledge base, which have a global behaviour just as the GCIs in T . Given an individual name a, it abides by a DCI C ∼ r D if at least one of the following three possibilities holds: (i) a is not in C; or (ii) a falls under C but there is another instance of C that is more preferred than a, or (iii) a is in D. This is captured by the or-like branch in the rule. Moreover, we need to check whether the node is not blocked in order to prevent the creation of an infinitely descending chain of increasingly more preferred objects. (This is needed to ensure termination of the algorithm and also that the preference relation on pairs of objects created when unraveling an open tableau is well-founded.)

The min-rule ensures that every individual that is more preferred than a typical instance of C is marked as an instance of ¬C.

Finally, the -rule takes care of completing ρ r A based on the information in σ r A so that the ordering on objects induced by that on pairs that ρ r A gives rise to coincides with the ordering on objects given by the strict version of σ r A . (See also Definition 3.) This is needed because at the end of the tableau execution, σ r A is discarded and only ρ r A is used to define an ordering on objects against which to check satisfiability of DCIs.

Definition 10 (Complete and clash-free ABox). Let A be an ABox. We say A contains a clash if there is some a ∈ I and C ∈ L dALC such that {a : C, a : ¬C} ⊆ A. We say A is clash-free if it does not contain a clash. A is complete if it contains a clash or if none of the expansion rules in Figure 4 is applicable to A.

Let ndexp(•) denote a function taking as input a clash-free ABox A, a nondeterministic rule R from Figure 4, and an assertion α ∈ A such that R is applicable to α in A. In our case, the nondeterministic rules are the -, ∃and ∼ -rules. The function returns a set ndexp(A, R, α) containing each of the possible ABoxes resulting from the application of R to α in A.

The tableau-based procedure for checking consistency of a dALC knowledge base KB = T ∪ D ∪ A is given in Algorithm 1 below. It uses Function Expand to apply the rules in Figure 4

Concluding Remarks

The tableau procedure presented here can be implemented as a proof procedure for checking consistency of contextual defeasible knowledge bases. It can also be used to perform preferential (and modular) entailment checking, and hence also used as part of an algorithm to determine rational closure. In its current form the complexity of the naïve procedure is doubly-exponential, with an optimal proof procedure currently under investigation.