=Paper=
{{Paper
|id=Vol-2373/paper-8
|storemode=property
|title=Reasoning with Contextual Defeasible ALC
|pdfUrl=https://ceur-ws.org/Vol-2373/paper-8.pdf
|volume=Vol-2373
|authors=Arina Britz,Ivan Varzinczak
|dblpUrl=https://dblp.org/rec/conf/dlog/BritzV19
}}
==Reasoning with Contextual Defeasible ALC==
https://ceur-ws.org/Vol-2373/paper-8.pdf
Reasoning with contextual defeasible ALC
Katarina Britz1 and Ivan Varzinczak2,1
1
CAIR, Stellenbosch University, South Africa
abritz@sun.ac.za
2
CRIL, Université d’Artois & CNRS, France
varzinczak@cril.fr
Abstract. In recent work, we addressed an important limitation in previous ex-
tensions of description logics to represent defeasible knowledge, namely the re-
striction in the semantics of defeasible concept inclusion to a single preference or-
der on objects of the domain. Syntactically, this limitation translates to a context-
agnostic 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) tableau-
based 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.
Keywords: description logics · defeasible reasoning · contexts · tableaux.
1 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 for-
malisms, DLs do not allow for the proper representation of and reasoning with defeasi-
ble 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 ap-
proaches [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
2 Britz and Varzinczak
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 contex-
tual 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.
2 Notation and an example
We assume finite and pairwise disjoint sets C, R and I standing for, respectively, con-
cept, 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 respec-
tive obvious intuitions. Complex concepts are denoted C, D, . . .
Figure 1 depicts an interpretation for our access-control example with domain ∆I =
{xi | 0 ≤ i ≤ 11}, and interpreting the elements of the vocabulary as follows:
ClassifiedI = {x10 }, EmployeeI = {x0 , x4 , x5 , x9 }, GraduateI = {x4 , x5 , x6 , x9 },
InternI = {x0 , x4 }, ResAssocI = {x5 , x6 , x7 }, hasAccI = {(x4 , x10 ), (x9 , x10 ),
(x6 , x10 ), (x6 , x11 )}, hasJobI = {(x0 , x3 ), (x4 , x3 ), (x9 , x3 ), (x5 , x1 ), (x6 , x1 )}, and
hasQuaI = {(x4 , x8 ), (x9 , x8 ), (x5 , x2 ), (x6 , x2 ), (x7 , x2 )}. 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 formal-
ising our access-control example:
Intern v Employee,
Employee v ∃hasJob.>,
Graduate v hasQua.>, anne : ResAssoc,
Employee v ∃hasAcc.Classified, chris : ResAssoc,
T = A=
Intern v ¬∃hasAcc.Classified,
doc123 : Classified,
Intern u Graduate v ∃hasAcc.Classified, (chris, doc123) : hasAcc
ResAssoc v ¬Employee,
ResAssoc v Graduate
It is not hard to see that this knowledge base is satisfiable and to check that KB |=
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 [15], of
which the intuition is “normally, C is subsumed by D”, formalised by the adoption of
Reasoning with contextual defeasible ALC 3
∆I EmpI
IntI
x0 (b) x1 x2
hQ
hJ hQ
hJ hQ
GradI
hJ
RAI
hJ
x3 x4 x5 (a) x6 (c) x7
hJ
hA
hQ hA hA
x8 x9 x10 (d) x11
hQ hA
ClassI
Fig. 1. An ALC interpretation for C, R and I as above. For the sake of presentation, concept, role
and individual names have been abbreviated.
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:
Employee @
∼ ∃hasAcc.Classified,
Intern @
Intern v Employee, ∼ ¬∃hasAcc.Classified,
@
T = Employee v ∃hasJob.>, D = Intern u Graduate ∼ ∃hasAcc.Classified,
Graduate v hasQua.> 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 classi-
cal 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 incom-
parable, 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. employ-
ment, 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 [12, 17]; defeasible concept inclusions [15], and context [18, 21].
4 Britz and Varzinczak
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 u C) | (C t C) | (∃r.C) | (∀r.C) | (−
∼|r.C) | (∼r.C)
W
−
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 (∼hasAcc.¬Classified) u (∃hasAcc.Classified), denoting those research
W
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 ∅ =6 X 0 ⊆ X,
0
min< X 6= ∅.
Definition 1 (Ordered interpretation). An ordered interpretation is a tuple O =def
h∆O , ·O , O i such that:
– h∆O , ·O i is an ALC interpretation, with AO ⊆ ∆O , for each A ∈ C, rO ⊆
∆O × ∆O , for each r ∈ R, and aO ∈ ∆O , for each a ∈ I, and
– O =def h O O O O O
r1 , . . . , r#R i, where ri ⊆ ri × ri , for i = 1, . . . , #R, and such
O
that each ri is a well-founded strict partial order.
Given O = h∆O , ·O , O i, the intuition of ∆O and ·O is the same as in a stan-
dard 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 in-
vestigated 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) ri .
Figure 2 depicts an ordered interpretation in our example, where ∆O and ·O are as in
the interpretation I shown in Figure 1, and O = h O O O
hasAcc , hasJob , hasQua i, where
O O
hasAcc = {(x6 x11 , x6 x10 )}, hasJob = {(x9 x3 , x0 x3 ), (x0 x3 , x4 x3 ), (x9 x3 , x4 x3 ),
(x0 x3 , x5 x1 ), (x9 x3 , x5 x1 ), (x6 x1 , x5 x1 )}, and O
hasQua = {(x5 x2 , x6 x2 ), (x6 x2 , x7 x2 ),
(x5 x2 , x7 x2 )}. (For the sake of readability, we shall henceforth sometimes write r-
tuples of the form (x, y) as xy.)
In the following definition we extend ordered interpretations to complex concepts
of the language.
Definition 2 (Interpretation of concepts). Let O = h∆O , ·O , O i, let r ∈ R and, for
each x ∈ ∆O , let rO|x =def rO ∩ ({x} × ∆O ) (i.e., the restriction of the domain of rO
Reasoning with contextual defeasible ALC 5
∆O EmpO
IntO
x0 (b) x1 x2
hQ
hJ hQ
hJ hQ
GradO
hJ
RAO
hJ
x3 x4 x5 (a) x6 (c) x7
hJ
hA
hQ hA hA
x8 x9 x10 (d) x11
hQ hA
ClassO
Fig. 2. An ordered interpretation. For the sake of presentation, we omit the transitive O
r -arrows.
to {x}). The interpretation function ·O interprets dALC concepts as follows:
>O =def ∆O ; ⊥O =def ∅; (¬C)O =def ∆O \ C O ;
(C u D)O =def C O ∩ DO ; (C t D)O =def C O ∪ DO ;
(∃r.C)O =def {x ∈ ∆O | rO (x) ∩ C O 6= ∅}; (∀r.C)O =def {x ∈ ∆O | rO (x) ⊆ C O };
(−
∼|r.C)O =def {x ∈ ∆O | min O (r O|x )(x) ∩ C O 6= ∅};
− r
(∼r.C)O =def {x ∈ ∆O | min O (rO|x )(x) ⊆ C O }.
W
r
Analogously to the classical case, ∼ and −
W
∼| are dual to each other. As an example, in
−
the ordered interpretation O of Figure 2, we have that (− ∼|hasAcc.Classified)O = ∅ =
−
(¬ ∼hasAcc.¬Classified) , whereas (∃hasAcc.Classified)O = {x6 }.
O
W
Defeasible ALC also adds contextual defeasible subsumption statements to knowl-
edge bases. Given C, D ∈ LdALC and r ∈ R, a statement of the form C @ ∼ r D is a (con-
textual) 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:
anne : Employee,
Intern v Employee, anne : ResAssoc,
Employee v ∃hasJob.>, bill : Intern,
T = A=
Graduate v hasQua.>,
chris : ResAssoc,
ResAssoc v ∼hasAcc.¬Classified
W
doc123 : Classified,
(chris, doc123) : hasAcc
6 Britz and Varzinczak
Employee @
∼ hasJob ∃hasAcc.Classified,
Intern @
¬∃hasAcc.Classified,
∼ hasJob
D = Intern u Graduate @∼ hasJob ∃hasAcc.Classified,
ResAssoc @ hasJob ¬Employee,
∼
ResAssoc @
Graduate
∼ hasQua
Definition 3 (Satisfaction). Let O = h∆O , ·O , O i, r ∈ R, C, D ∈ LdALC , and
a, b ∈ I. Define ≺O O O
r ⊆ ∆ × ∆ as follows:
≺O O O O
r =def {(x, y) | there is (x, z) ∈ r s.t. for all (y, v) ∈ r , ((x, z), (y, v)) ∈ r }.
The satisfaction relation is defined as follows:
O CvD if C O ⊆ DO ; O C@
∼ rD if min≺O
r
C O ⊆ DO ;
O a:C if aO ∈ C O ; O (a, b) : r if (aO , bO ) ∈ rO .
If O α, then we say O satisfies α. O satisfies a dALC knowledge base KB, written
O KB, if O α for every α ∈ 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 ∈ LdALC (resp.
r ∈ R) is satisfiable w.r.t. KB if there is a model O of KB s.t. C O 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 (repre-
sented with dotted arrows) induced from those on roles in O as specified in Definition 3.
∆O EmpO
IntO
x0 (b) x1 x2
hQ
hJ hQ
hJ hJ hQ
GradO
hJ
hJ RAO
hJ hQ hQ
x3 x4 x5 (a) x6 (c) x7
hJ
hJ
hJ hA
hQ hA hA
x8 x9 x10 (d) x11
hQ hA
ClassO
Fig. 3. Induced orderings on objects from the role orderings in Figure 2. For the sake of presen-
tation, we omit the transitive ≺O
r -arrows.
It follows from Definition 3 that, if Or = ∅, 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 ∃r.>)O = ∅, then C @ ∼ r D reverts to C v D.
This reflects the intuition that the context r is taken into account through the preference
Reasoning with contextual defeasible ALC 7
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 subsump-
tion based on a preference order on objects in the domain of rO obtained from O r .
Non-contextual defeasible subsumption can then be obtained as a special case by intro-
ducing a new role name r and axiom > v ∃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 as-
sertions 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 ∈ LdALC , KB |= C v D iff KB |= C u ¬D v ⊥ iff
KB ∪ {a : C u ¬D} is unsatisfiable. Moreover, for every b ∈ I and every C ∈ LdALC ,
KB |= b : C iff KB ∪ {b : ¬C} 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 de-
ciding 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. [4]
in the classical case.
We start by observing that, for every ordered interpretation O and every C, D ∈
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 ∈ 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 ∈ LdALC . The set of subconcepts of C, denoted
sub(C), is defined inductively as follows:
– If C = A, for A ∈ C ∪ {>, ⊥}, then sub(C) =def {A};
– If C = C1 u C2 or C = C1 t C2 , then sub(C) =def {C} ∪ sub(C1 ) ∪ sub(C2 );
8 Britz and Varzinczak
– If C = ¬D or C = ∃r.D or C = ∀r.D or C = −
∼|r.D or C = ∼r.D, then
W
−
sub(C) =def {C} ∪ 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
S S
sub(T ) =def CvD∈T (sub(C) ∪ sub(D)) sub(A) =def a:C∈A sub(C)
S
sub(D) =def C @ D∈D (sub(C) ∪ sub(D))
∼ r
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 ∈ LdALC , r ∈ R and b ∈ I.
Definition 6 (a-concepts). Let A be an ABox and let a be an individual name appear-
ing in A. With conA (a) =def {C | a : C ∈ A} 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-, ∀-, 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.
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 ∈ 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 clash-
free ABox (see below), if there is any, ρrA is used to define a preference relation on the
interpretation of role r in the constructed ordered interpretation.
r
The second auxiliary structure is a pre-order σ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 ρrA -ordering can be completed (by the -rule) and, in the un-
r
ravelling of the model, deliver an induced ≺r that is faithful to σA . (This point will
be made more clearly in the explanation of the relevant rules. In particular, the reason
r
why σA is a pre-order and not a partial order like ρrA will be explained in the soundness
r
proof.) Intuitively, σA corresponds to the converse of the preference order introduced
in Definition 3.
r
Finally, the third structure used in the expansion rules is a labelling function τA (a)
mapping an individual name a to the set of concepts a ought to be a minimal instance
r
of in the context r w.r.t. the ABox A. The purpose of τ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
Reasoning with contextual defeasible ALC 9
r
normal elements in σA . Note that ρrA , σA
r r
and τA (a) are only used in the inner workings
of the tableau and are not accessible to the user.
Definition 7 (r-ancestor). Let A be an ABox, a, b ∈ I, and r ∈ R. If (a, b) : r ∈ 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).
r r
Definition 8 (σA -ancestor). Let A be an ABox, a, b ∈ I, and r ∈ R. If (a, b) ∈ σA ,
r r
we say b is a σA -successor of a and a is an σA -predecessor of b. The transitive closure
r r r r
of the σA -predecessor (resp. σA -successor) relation is called σA -ancestor (resp. σA -
descendant).
r
An individual is called a root if it has neither an r-ancestor nor a σA -ancestor.
u-rule: if 1. a : C u D ∈ A, and
2. {a : C, a : D} 6⊆ A
then A := A ∪ {a : C, a : D}
t-rule: if 1. a : C t D ∈ A, and
2. {a : C, a : D} ∩ A = ∅
then A := A ∪ {a : E}, for some E ∈ {C, D}
∃-rule: if 1. a : ∃r.C ∈ A, and
2. there is no b s.t. {(a, b) : r, b : C} ⊆ A, and
3. a is not blocked
then (a) A := A ∪ {(a, c) : r, c : C}, for c new in A, or
(b) A := A ∪ {(a, c) : r, c : C, (a, d) : r}, for c, d new in A, and ρrA := ρrA ∪ {(ad, ac)}
∀-rule: if 1. {a : ∀r.C, (a, b) : r} ⊆ A, and
2. b : C ∈/A
then A := A ∪ {b : C}
−
∼|-rule:
− if 1. a : −
∼|r.C ∈ A, and
−
2. there is no b s.t. (i) {(a, b) : r, b : C} ⊆ A, and (ii) there is no c s.t. (ac, ab) ∈ ρrA , and
3. a is not blocked
then A := A ∪ {(a, d) : r, d : C}, for d new in A
∼-rule: if 1. {a : ∼r.C, (a, b) : r} ⊆ A, and
W W
2. there is no c s.t. (ac, ab) ∈ ρrA , and
3. b : C ∈/A
then A := A ∪ {b : C}
T -rule: if 1. a appears in A, > v D ∈ T , and
2. a : D ∈ /A
then A := A ∪ {a : D}
@∼ -rule: if 1. a appears in A, C @ ∼ r D ∈ D, and
2. {a : ¬C, a : D} ∩ A = ∅, and
r
3. either a : C ∈ / A or there is no b s.t. b : C ∈ A and (a, b) ∈ σA , and
4. a is not blocked
then (a) A := A ∪ {a : ¬C}, or
r r r
(b) A := A ∪ {a : C, c : C, c : D}, for c new in A, σA := σA ∪ {(a, c)}, and τA (c) := {C} or
(c) A := A ∪ {a : D}
r
min-rule: if 1. C ∈ τA (a), and
r +
2. b : ¬C ∈ / A, for some b s.t. (a, b) ∈ (σA )
then A := A ∪ {b : ¬C}
r
-rule: if 1. (b, a) ∈ σA , and
2. there is no c s.t. (ac, bd) ∈ ρrA for every (b, d) : r ∈ A, and
3. a is not blocked
then A := A ∪ {(a, e) : r}, for e new in A, and ρrA := ρrA ∪ {(ae, bf ) | (b, f ) : r ∈ A}
Fig. 4. Expansion rules for the dALC tableau.
The following definition is used in the expansion rules of Figure 4 to ensure termination:
10 Britz and Varzinczak
r r
Definition 9 (Blocking). Let A be an ABox, a, b ∈ I, and let σA and τ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 r r
σA -ancestor of b, (2) conA (b) ⊆ conA (a), and (3) τA (b) ⊆ τA (a). We say b is blocked
r
in A if itself or some r-ancestor or σA -ancestor of b is blocked by some individual.
The u-, t-, ∀-, 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 indi-
−
vidual 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) ∈ ρrA .
The ∼-rule is analogous to the ∀-rule, but propagates a concept C only to those
W
individuals across preferred r-links (i.e., r-links that are minimal in ρrA ).
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 ρ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@ ∼ 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 ρrA based on the information in σA r
so
r
that the ordering on objects induced by that on pairs that ρA gives rise to coincides with
r
the ordering on objects given by the strict version of σA . (See also Definition 3.) This
r
is needed because at the end of the tableau execution, σA is discarded and only ρrA 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 ∈ LdALC 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 nondeter-
ministic 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 t-, ∃- 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 to A w.r.t. T and D. Given an ABox A, with ρA , σA and τA we denote,
r r r
respectively, the sequences hρrA1 , . . . , ρA#R i, hσA
r1 r1
, . . . , σA#R i and hτA , . . . , τA#R i.
Reasoning with contextual defeasible ALC 11
Algorithm 1: Consistent(KB)
Input: A dALC knowledge base KB = T ∪ D ∪ A
1 if Expand(KB) 6= ∅ then
2 return “Consistent”
3 else
4 return “Inconsistent”
Function Expand(KB)
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 α ∈ A to which R is applicable;
5 if there is A0 ∈ ndexp(A, R, α) with Expand(T ∪ D ∪ A0 ) 6= ∅ then
6 return Expand(T ∪ D ∪ A0 )
7 else
8 return ∅
9 else
10 Apply R to A
11 if A contains a clash then
12 return ∅
13 else
14 return hA, ρA , σA , τA i
Lemma 2 (Termination). For every knowledge base KB, Consistent(KB) terminates.
The proof of Lemma 2 is similar to that showing termination of the classical ALC
tableau for checking consistency of general knowledge bases [4, Lemma 4.10].
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.
12 Britz and Varzinczak
References
1. Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P. (eds.): The De-
scription Logic Handbook: Theory, Implementation and Applications. Cambridge University
Press, 2 edn. (2007)
2. Baader, F., Hollunder, B.: How to prefer more specific defaults in terminological default
logic. In: Bajcsy, R. (ed.) Proceedings of the 13th International Joint Conference on Artificial
Intelligence (IJCAI). pp. 669–675. Morgan Kaufmann Publishers (1993)
3. Baader, F., Hollunder, B.: Embedding defaults into terminological knowledge representation
formalisms. Journal of Automated Reasoning 14(1), 149–180 (1995)
4. Baader, F., Horrocks, I., Lutz, C., Sattler, U.: An Introduction to Description Logic. Cam-
bridge University Press (2017)
5. Bonatti, P., Faella, M., Petrova, I., Sauro, L.: A new semantics for overriding in description
logics. Artificial Intelligence 222, 1–48 (2015)
6. Bonatti, P., Faella, M., Sauro, L.: Defeasible inclusions in low-complexity DLs. Journal of
Artificial Intelligence Research 42, 719–764 (2011)
7. Bonatti, P., Lutz, C., Wolter, F.: The complexity of circumscription in description logic. Jour-
nal of Artificial Intelligence Research 35, 717–773 (2009)
8. Booth, R., Casini, G., Meyer, T., Varzinczak, I.: On the entailment problem for a logic of typ-
icality. In: Proceedings of the 24th International Joint Conference on Artificial Intelligence
(IJCAI). pp. 2805–2811 (2015)
9. Booth, R., Meyer, T., Varzinczak, I.: PTL: A propositional typicality logic. In: Fariñas del
Cerro, L., Herzig, A., Mengin, J. (eds.) Proceedings of the 13th European Conference on
Logics in Artificial Intelligence (JELIA). pp. 107–119. No. 7519 in LNCS, Springer (2012)
10. Booth, R., Meyer, T., Varzinczak, I.: A propositional typicality logic for extending rational
consequence. In: Fermé, E., Gabbay, D., Simari, G. (eds.) Trends in Belief Revision and
Argumentation Dynamics, Studies in Logic – Logic and Cognitive Systems, vol. 48, pp.
123–154. King’s College Publications (2013)
11. Boutilier, C.: Conditional logics of normality: A modal approach. Artificial Intelligence
68(1), 87–154 (1994)
12. Britz, K., Casini, G., Meyer, T., Varzinczak, I.: Preferential role restrictions. In: Proceedings
of the 26th International Workshop on Description Logics. pp. 93–106 (2013)
13. Britz, K., Heidema, J., Meyer, T.: Semantic preferential subsumption. In: Lang, J., Brewka,
G. (eds.) Proceedings of the 11th International Conference on Principles of Knowledge Rep-
resentation and Reasoning (KR). pp. 476–484. AAAI Press/MIT Press (2008)
14. Britz, K., Heidema, J., Meyer, T.: Modelling object typicality in description logics. In:
Nicholson, A., Li, X. (eds.) Proceedings of the 22nd Australasian Joint Conference on Arti-
ficial Intelligence. pp. 506–516. No. 5866 in LNAI, Springer (2009)
15. Britz, K., Meyer, T., Varzinczak, I.: Semantic foundation for preferential description logics.
In: Wang, D., Reynolds, M. (eds.) Proceedings of the 24th Australasian Joint Conference on
Artificial Intelligence. pp. 491–500. No. 7106 in LNAI, Springer (2011)
16. Britz, K., Varzinczak, I.: Defeasible modalities. In: Proceedings of the 14th Conference on
Theoretical Aspects of Rationality and Knowledge (TARK). pp. 49–60 (2013)
17. Britz, K., Varzinczak, I.: Introducing role defeasibility in description logics. In: Michael,
L., Kakas, A. (eds.) Proceedings of the 15th European Conference on Logics in Artificial
Intelligence (JELIA). pp. 174–189. No. 10021 in LNCS, Springer (2016)
18. Britz, K., Varzinczak, I.: Context-based defeasible subsumption for dSROIQ. In: Proceed-
ings of the 13th International Symposium on Logical Formalizations of Commonsense Rea-
soning (2017)
Reasoning with contextual defeasible ALC 13
19. Britz, K., Varzinczak, I.: From KLM-style conditionals to defeasible modalities, and back.
Journal of Applied Non-Classical Logics (JANCL) 28(1), 92–121 (2018)
20. Britz, K., Varzinczak, I.: Preferential accessibility and preferred worlds. Journal of Logic,
Language and Information (JoLLI) 27(2), 133–155 (2018)
21. Britz, K., Varzinczak, I.: Rationality and context in defeasible subsumption. In: Ferrarotti,
F., Woltran, S. (eds.) Proceedings of the 10th International Symposium on Foundations of
Information and Knowledge Systems (FoIKS). pp. 114–132. No. 10833 in LNCS, Springer
(2018)
22. Casini, G., Meyer, T., Moodley, K., Sattler, U., Varzinczak, I.: Introducing defeasibility into
OWL ontologies. In: Arenas, M., Corcho, O., Simperl, E., Strohmaier, M., d’Aquin, M.,
Srinivas, K., Groth, P., Dumontier, M., Heflin, J., Thirunarayan, K., Staab, S. (eds.) Proceed-
ings of the 14th International Semantic Web Conference (ISWC). pp. 409–426. No. 9367 in
LNCS, Springer (2015)
23. Casini, G., Straccia, U.: Rational closure for defeasible description logics. In: Janhunen,
T., Niemelä, I. (eds.) Proceedings of the 12th European Conference on Logics in Artificial
Intelligence (JELIA). pp. 77–90. No. 6341 in LNCS, Springer-Verlag (2010)
24. Casini, G., Straccia, U.: Defeasible inheritance-based description logics. Journal of Artificial
Intelligence Research (JAIR) 48, 415–473 (2013)
25. Donini, F., Nardi, D., Rosati, R.: Description logics of minimal knowledge and negation as
failure. ACM Transactions on Computational Logic 3(2), 177–225 (2002)
26. Giordano, L., Gliozzi, V., Olivetti, N., Pozzato, G.: Preferential description logics. In: Der-
showitz, N., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Rea-
soning (LPAR). pp. 257–272. No. 4790 in LNAI, Springer (2007)
27. Giordano, L., Gliozzi, V., Olivetti, N., Pozzato, G.: Reasoning about typicality in preferential
description logics. In: Hölldobler, S., Lutz, C., Wansing, H. (eds.) Proceedings of the 11th
European Conference on Logics in Artificial Intelligence (JELIA). pp. 192–205. No. 5293
in LNAI, Springer (2008)
28. Giordano, L., Gliozzi, V., Olivetti, N., Pozzato, G.: ALC + T : a preferential extension of
description logics. Fundamenta Informaticae 96(3), 341–372 (2009)
29. Giordano, L., Gliozzi, V., Olivetti, N., Pozzato, G.: A non-monotonic description logic for
reasoning about typicality. Artificial Intelligence 195, 165–202 (2013)
30. Giordano, L., Gliozzi, V., Olivetti, N., Pozzato, G.: Semantic characterization of rational clo-
sure: From propositional logic to description logics. Artificial Intelligence 226, 1–33 (2015)
31. Governatori, G.: Defeasible description logics. In: Antoniou, G., Boley, H. (eds.) Rules and
Rule Markup Languages for the Semantic Web. pp. 98–112. No. 3323 in LNCS, Springer
(2004)
32. Grosof, B., Horrocks, I., Volz, R., Decker, S.: Description logic programs: Combining logic
programs with description logic. In: Proceedings of the 12th International Conference on
World Wide Web (WWW). pp. 48–57. ACM (2003)
33. Heymans, S., Vermeir, D.: A defeasible ontology language. In: Meersman, R., Tari, Z. (eds.)
CoopIS/DOA/ODBASE. pp. 1033–1046. No. 2519 in LNCS, Springer (2002)
34. Kraus, S., Lehmann, D., Magidor, M.: Nonmonotonic reasoning, preferential models and
cumulative logics. Artificial Intelligence 44, 167–207 (1990)
35. Lehmann, D., Magidor, M.: What does a conditional knowledge base entail? Artificial Intel-
ligence 55, 1–60 (1992)
36. Padgham, L., Zhang, T.: A terminological logic with defaults: A definition and an applica-
tion. In: Bajcsy, R. (ed.) Proceedings of the 13th International Joint Conference on Artificial
Intelligence (IJCAI). pp. 662–668. Morgan Kaufmann Publishers (1993)
37. Qi, G., Pan, J., Ji, Q.: Extending description logics with uncertainty reasoning in possibilistic
logic. In: Mellouli, K. (ed.) Proceedings of the 9th European Conference on Symbolic and
14 Britz and Varzinczak
Quantitative Approaches to Reasoning with Uncertainty. pp. 828–839. No. 4724 in LNAI,
Springer (2007)
38. Quantz, J., Royer, V.: A preference semantics for defaults in terminological logics. In: Pro-
ceedings of the 3rd International Conference on Principles of Knowledge Representation and
Reasoning (KR). pp. 294–305 (1992)
39. Quantz, J., Ryan, M.: Preferential default description logics. Tech. rep., TU Berlin (1993),
www.tu-berlin.de/fileadmin/fg53/KIT-Reports/r110.pdf
40. Sengupta, K., Alfa Krisnadhi, A., Hitzler, P.: Local closed world semantics: Grounded cir-
cumscription for OWL. In: Aroyo, L., Welty, C., Alani, H., Taylor, J., Bernstein, A., Kagal,
L., Noy, N., Blomqvist, E. (eds.) Proceedings of the 10th International Semantic Web Con-
ference (ISWC). pp. 617–632. No. 7031 in LNCS, Springer (2011)
41. Shoham, Y.: Reasoning about Change: Time and Causation from the Standpoint of Artificial
Intelligence. MIT Press (1988)
42. Straccia, U.: Default inheritance reasoning in hybrid KL-ONE-style logics. In: Bajcsy, R.
(ed.) Proceedings of the 13th International Joint Conference on Artificial Intelligence (IJ-
CAI). pp. 676–681. Morgan Kaufmann Publishers (1993)
43. Varzinczak, I.: A note on a description logic of concept and role typicality for defeasible
reasoning over ontologies. Logica Universalis 12(3-4), 297–325 (2018)