In recent work, we addressed an important limitation in previous extensions of description logics to represent defeasible knowledge, namely the restriction in the semantics of defeasible concept inclusion to a single preference order on objects of the domain. Syntactically, this limitation translates to a contextagnostic notion of defeasible subsumption, which is quite restrictive when it comes to modelling different nuances of defeasibility. Our point of departure in our recent proposal allows for different orderings on the interpretation of roles. This yields a notion of contextual defeasible subsumption, where the context is informed by a role. In the present paper, we extend this work to also provide a proof-theoretic counterpart and associated results. We define a (naïve) tableaubased algorithm for checking preferential consistency of contextual defeasible knowledge bases, a central piece in the definition of other forms of contextual defeasible reasoning over ontologies, notably contextual rational closure.
Description logics (DLs) [
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 [
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 [
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. 2
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 = fClassi ed; Employee; Graduate; Intern; ResAssocg, R = fhasAcc; hasJob; hasQuag, and I = fanne; bill; chris; doc123g, with the respective obvious intuitions. Complex concepts are denoted C; D; : : :
Figure 1 depicts an interpretation for our access-control example with domain I = fxi j 0 i 11g, and interpreting the elements of the vocabulary as follows: Classi edI = fx10g, EmployeeI = fx0; x4; x5; x9g, GraduateI = fx4; x5; x6; x9g, InternI = fx0; x4g, ResAssocI = fx5; x6; x7g, hasAccI = f(x4; x10); (x9; x10); (x6; x10); (x6; x11)g, hasJobI = f(x0; x3); (x4; x3); (x9; x3); (x5; x1); (x6; x1)g, and hasQuaI = f(x4; x8); (x9; x8); (x5; x2); (x6; x2); (x7; x2)g. Further, anneI = x5, billI = x0, chrisI = x6, and doc123I = x10.
The knowledge base KB = T [ A, with T and A as below, is a first stab at formalising our access-control example: T = 8 > > > > > > > > > > <
Employee v 9hasJob:>;
Graduate v hasQua:>;
Employee v 9hasAcc:Classi ed; > Intern v :9hasAcc:Classi ed; > >>> Intern u Graduate v 9hasAcc:Classi ed; >>> >>:>>>> RReseAs Asssoscocvv:GErmadpuloayteee; ;>>>>>> 9 > > > > > > > > > > =
A =
It is not hard to see that this knowledge base is satisfiable and to check that KB j=
Intern v ?. 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 [
EmpI x0(b)
IntI x4 x9 hA hA x1 hJ x5(a) hJ hQ
hA
a preferential semantics à la Shoham [
Employee v 9hasJob:>; : Graduate v hasQua:> ;
D =
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. 3
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 [
Let C, R and I be as before. Complex dALC concepts are denoted C; D; : : :, and are built according to the rules:
C ::= > j ? j C j (:C) j (C u C) j (C t C) j (9r:C) j (8r:C) j ( |r:C) j (Wr:C)
With LdALC we denote the language of all dALC concepts (including all ALC concepts). Again, when writing down elements of LdALC , we shall omit parentheses whenever they are not necessary for disambiguation. An example of dALC concept is ResAssoc u (WhasAcc::Classi ed) u (9hasAcc:Classi ed), 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 [
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 fx 2 X j there is no y 2 X s.t. y < xg we denote the minimal elements of X w.r.t. <. A strict partial order on a set X is well-founded if for every ; =6 X0 X, min< X0 6= ;.
Definition 1 (Ordered interpretation). An ordered interpretation is a tuple O =def h O; O; Oi such that: – h –
O; Oi is an ALC interpretation, with AO O, for each A 2 C, rO O O, for each r 2 R, and aO 2 O, for each a 2 I, and
O=def h rO1 ; : : : ; rO#R i, where rOi riO riO, for i = 1; : : : ; #R, and such that each rOi is a well-founded strict partial order.
Given O = h O; O; Oi, 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 [
EmpO
IntO x4 x9 hA hA ClassO
GradO hQ hA x11 x7
RAO to fxg). The interpretation function O interprets dALC concepts as follows: >O =def
O; ?O =def ;; (:C)O =def
O n CO; (C u D)O =def CO \ DO;
(C t D)O =def CO [ DO; (9r:C)O =def fx 2 ( |r:C)O =def fx 2 (Wr:C)O =def fx 2
O j rO(x) \ CO 6= ;g; (8r:C)O =def fx 2 O j rO(x)
COg; O j min rO (rOjx)(x) \ CO 6= ;g; O j min rO (rOjx)(x)
COg:
Analogously to the classical case, W and | are dual to each other. As an example, in the ordered interpretation O of Figure 2, we have that ( |hasAcc:Classi ed)O = ; = (: WhasAcc::Classi ed)O, whereas (9hasAcc:Classi ed)O = fx6g.
Defeasible ALC also adds contextual defeasible subsumption statements to knowledge bases. Given C; D 2 LdALC and r 2 R, a statement of the form C @ rD 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 v 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 =
Employee v 9hasJob:>; > Graduate v hasQua:>; > >: ResAssoc v WhasAcc::Classi ed ;>
D = rO =def f(x; y) j there is (x; z) 2 rO s.t. for all (y; v) 2 rO; ((x; z); (y; v)) 2 rOg: The satisfaction relation
is defined as follows: O O
C v D a : C if
CO
DO; if aO 2 CO;
O O min O CO
r (aO; bO) 2 rO:
DO; If O , then we say O satisfies . O satisfies a dALC knowledge base KB, written O KB, if O for every 2 KB, in which case we say O is a model of KB. We say KB is preferentially consistent if it admits a model. We say C 2 LdALC (resp. r 2 R) is satisfiable w.r.t. KB if there is a model O of KB s.t. CO 6= ; (resp. rO 6= ;).
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.
O
EmpO x3 x8
IntO
ClassO x2 hQ
GradO hQ hA x11 hQ x6(c) hQ x7
RAO
It follows from Definition 3 that, if rO= ;, i.e., if no r-tuple is preferred to another, then @ r reverts to a context-agnostic classical v. A similar observation holds for individual concept inclusions: if (C u 9r:>)O = ;, then C @ rD reverts to C v D. This reflects the intuition that the context r is taken into account through the preference order on rO. 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 v.
Contextual defeasible subsumption @ r can also be viewed as defeasible subsumption based on a preference order on objects in the domain of rO obtained from rO. Non-contextual defeasible subsumption can then be obtained as a special case by introducing a new role name r and axiom > v 9r:>.
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 dALC knowledge base KB, written KB j=pref , if O is preferentially entailed by a 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: Lemma 1. Let KB be a dALC knowledge base and let a be an individual name not occurring in KB. For every C; D 2 LdALC , KB j= C v D iff KB j= C u :D v ? iff KB [ fa : C u :Dg is unsatisfiable. Moreover, for every b 2 I and every C 2 LdALC , KB j= b : C iff KB [ fb : :Cg is unsatisfiable.
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. 4
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. [
We start by observing that, for every ordered interpretation O and every C; D 2 LdALC , O C v D if and only if O > v :C t D. In that respect, we can assume w.l.o.g. that all GCIs in a TBox are of the form > v E, for some E 2 LdALC .
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 2 LdALC . The set of subconcepts of C, denoted sub(C), is defined inductively as follows: – If C = A, for A 2 C [ f>; ?g, then sub(C) =def fAg; – If C = C1 u C2 or C = C1 t C2, then sub(C) =def fCg [ sub(C1) [ sub(C2); – If C = :D or C = 9r:D or C = 8r:D or C = |r:D or C = Wr:D, then sub(C) =def fCg [ sub(D).
Given a knowledge base KB = T [ D [ A, the set of subconcepts of KB is defined as sub(KB) =def sub(T ) [ sub(D) [ sub(A), where sub(T ) =def SCvD2T (sub(C) [ sub(D)) sub(A) =def Sa:C2A sub(C)
(sub(C) [ sub(D))
We say that an individual name a appears in an ABox A if A contains an assertion of the form a : C, (a; b) : r or (b; a) : r, for some C 2 LdALC , r 2 R and b 2 I. Definition 6 (a-concepts). Let A be an ABox and let a be an individual name appearing in A. With conA(a) =def fC j a : C 2 Ag we denote the set of concepts that a is an instance of w.r.t. A.
We are now ready for the definition of the expansion rules for dALC-concepts. They
are shown in Figure 4. The u-, t-, 8-, and T -rules work as in the classical case [
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 rA, for each r 2 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 is used to define a preference relation on the
A interpretation of role r in the constructed ordered interpretation.
The second auxiliary structure is a pre-order Ar on individual names, for each r 2 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) rsaovtehllaitngtheofatshseocmiaoteddel, rAde-olirvdeerrianngicnadnucbeed comrpthleatteids (fbayiththfuel to-ruArle.)(Tanhdis, ipnoitnhte wuinl-l be made more clearly in the explanation of the relevant rules. In particular, the reason why Ar is a pre-order and not a partial order like rA will be explained in the soundness proof.) Intuitively, r corresponds to the converse of the preference order introduced
A in Definition 3.
Finally, the third structure used in the expansion rules is a labelling function Ar(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 Ar(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 . Note that r , r and r (a) are only used in the inner workings
A A A A of the tableau and are not accessible to the user.
Definition 7 (r-ancestor). Let A be an ABox, a; b 2 I, and r 2 R. If (a; b) : r 2 A, we say b is an r-successor of a and a is an r-predecessor of b. The transitive closure of the r-predecessor (resp. r-successor) relation is called r-ancestor (resp. r-descendant). Definition 8 ( r -ancestor). Let A be an ABox, a; b 2 I, and r 2 R. If (a; b) 2 r , we say b is a r A-successor of a and a is an r -predecessor of b. The transitive closure A of the r -predAecessor (resp. r -successor) rAelation is called r -ancestor (resp. r
A A A A descendant).
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 2 I, and let r and r be as above. A A We say that b is blocked by a in A in the context r if (1) a is either an r-ancestor or a inArA-ainfcietssetolfroorf sbo, m(2e) rc-oannAce(bst)or ocronrA-(aan)c,easntdor(3o)f bAris(bb)lockeAdr(bay).soWmeesainydbiviisdbulaolc.ked
A
The u-, t-, 8-, 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) 2 rA.
The W-rule is analogous to the 8-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 9-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 rA).
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 @ rD 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 rA based on the information in Ar so that the ordering on objects induced by that on pairs that r gives rise to coincides with itsheneoerddeerdinbgecoanusoebjaetctthsegievnednobfyt htheetasbtrliecatuveerxseicountioofn, ArAr.A(SisedeiasclsaordDedefiannidtioonnl3y.) TrAhiiss 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 2 I and C 2 LdALC such that fa : C; a : :Cg 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 2 A such that R is applicable to in A. In our case, the nondeterministic rules are the t-, 9- 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 respectively, the sequences h A . Given an Ar1B; o:x:: A; Ar#R i and h A A i rules in Figure 4 to A w.r.t. T arn1;d: D:: ; rA#R i, h A , with A, Ar1a;n:d: : A; wr#eRde.note,
Input: A dALC knowledge base KB = T [ D [ A 1 if Expand(KB) 6= ; then 2 return “Consistent” 3 else 4
return “Inconsistent”
Input: A dALC knowledge base KB = T [ D [ A 1 if A is not complete then 2 Select a rule R that is applicable to A; 3 if R is a nondeterministic rule then 4 Select an assertion 2 A to which R is applicable; 5 if there is A0 2 ndexp(A; R; ) with Expand(T [ D [ A0) 6= ; then 6 return Expand(T [ D [ A0) Theorem 1. Algorithm 1 is sound and complete w.r.t. preferential consistency of dALC knowledge bases.
Corollary 1. Our tableau-based algorithm is a decision procedure for satisfiability of dALC knowledge bases. 5
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.