=Paper=
{{Paper
|id=Vol-1195/long9
|storemode=property
|title=Defeasibility in Contextual Reasoning with CKR
|pdfUrl=https://ceur-ws.org/Vol-1195/long9.pdf
|volume=Vol-1195
|dblpUrl=https://dblp.org/rec/conf/cilc/BozzatoES14
}}
==Defeasibility in Contextual Reasoning with CKR==
https://ceur-ws.org/Vol-1195/long9.pdf
Defeasibility in contextual reasoning with CKR?
Loris Bozzato1 , Thomas Eiter2 , and Luciano Serafini1
1
Fondazione Bruno Kessler, Via Sommarive 18, 38123 Trento, Italy
2
Institut für Informationssysteme, Technische Universität Wien,
Favoritenstraße 9-11, A-1040 Vienna, Austria
{bozzato,serafini}@fbk.eu, eiter@kr.tuwien.ac.at
Abstract. Recently, representation of context dependent knowledge in the Se-
mantic Web has been recognized as a relevant issue and a number of logic based
solutions have been proposed in this regard: among them, in our previous works
we presented the Contextualized Knowledge Repository (CKR) framework.
A CKR knowledge base has a two layered structure, modelled by a global context
and a set of local contexts: the global context not only contains the metaknowl-
edge defining the properties of local contexts, but also holds the global (context
independent) object knowledge that is shared by all of the local contexts. In many
practical cases, however, it is desirable to leave the possibility to “override” the
global object knowledge at the local level, by recognizing the axioms that can
allow exceptional instances in the local contexts. This clearly requires to add a
notion of non monotonicity across the global and the local parts of a CKR.
In this paper we present an extension to the semantics of CKR to introduce such
notion of defeasible axioms. By extending a previously proposed datalog trans-
lation, we obtain a representation for CKR as a datalog program with negation
under answer set semantics. This representation can be exploited as the basis for
implementation of query answering for the proposed extension of CKR.
1 Introduction
Representation of context dependent knowledge in the Semantic Web has been recently
recognized as a relevant issue that lead to a number of logic based proposals, e.g. [7–9,
13–15, 12]; in particular, the Contextualized Knowledge Repository (CKR) framework
[12, 3, 2], with its latest formulation in [4], has been developed at the FBK in Trento.
A CKR knowledge base has a two layered structure: basically, it consists of a global
context and a set of local contexts. The global context contains metaknowledge defin-
ing the properties of local contexts, as well as the global (context independent) object
knowledge that is shared by all of the local contexts. Local contexts, on the other hand,
contain knowledge that holds under specific circumstances (e.g. an event) and thus rep-
resent different independent views of the domain. The global object knowledge is prop-
agated from the global to the local contexts and used as a common part of the system
knowledge. In many practical cases, however, it is desirable to leave the possibility to
“override” the global object knowledge at the local level, by recognizing those axioms
that can allow exceptional instances in their local instantiations.
?
This paper has been previously presented at the 5th International Workshop on Acquisition,
Representation and Reasoning with Contextualized Knowledge (ARCOE-LogIC 2013).
132
L. Bozzato, T. Eiter, L. Serafini. Defeasibility in contextual reasoning with CKR
For example, in the scenario of an event recommendation system, we might want
to assert at the global level that “by default, all of the cheap events are interesting”,
but then override this inclusion for particular kind of events in the context of a partic-
ipant. We might also want to express defeasibility on the propagation of information:
for instance, in a CKR representing an organization, we might want to express that “by
default, all the employees working the previous year also work in the current year”
and override the axiom in the context of a specific year for employees that finished
their working contract at that time. In other words, we want to specify that certain ax-
ioms at the global level are defeasible, thus they can allow exceptional instances in
local contexts, while holding in the general case: this clearly requires to add a notion of
non-monotonicity across the global and the local parts of a CKR.
In this work, we present an extension to the CKR semantics of [4] to support such
defeasibility for global object knowledge. We desire to enrich previous work and to
have a datalog representation of the extended CKR semantics that extends the one for
the CKR semantics in [4]: we introduced defeasible axioms guided by the approach of
inheritance logic programs in [5]. There the idea is that special rules recognize excep-
tional facts at the local level and others propagate global facts only if they are not proved
to be overridden at the local level, which happens if the opposite is derived; in the same
vein, we consider instances of axioms that might be overridden at the local level. The
semantics for CKR we define is (as desired) representable by a datalog program with
negation under answer sets semantics; furthermore, a respective translation can be used
as the basis to implement query answering over defeasible CKR knowledge bases.
We can thus summarize the contributions of our work as follows. After a brief in-
troduction of preliminary definitions in Section 2, we present in Section 3 syntax and
semantics of an extension of CKR with defeasible axioms in the global context. No-
tably, this allow us to introduce for the first time a notion of non-monotonicity across
contexts in our contextual framework. We then extend in Section 4 the datalog trans-
lation for OWL RL based CKR from [4] with rules for the translation of defeasible
axioms and for considering local exceptions in the propagation of such knowledge. We
express non-monotonicity using answer set semantics, such that instance checking over
an CKR with defeasible axioms reduces to cautious inference from all answer set of the
translation. The work reported here is in progress, and an implementation of a prototype
reasoner, based on the results of [4] and this paper, is underway.
2 Preliminaries: SROIQ-RL
This work basically builds on the materialization calculus for CKR on OWL RL re-
cently proposed in [4]. The extension of the calculus that we present here is again for-
mulated over the language SROIQ-RL, which represents the restriction of SROIQ
to the OWL RL constructs [11]. The language is obtained by restricting the form of Gen-
eral Concept Inclusion axioms (GCIs) and concept equivalence of SROIQ to C v D
where C and D are concept expressions, called left-side concept and right-side concept
respectively, and defined by the following grammar:
C := A | {a} | C1 u C2 | C1 t C2 | 9R.C1 | 9R.{a} | 9R.>
D := A | ¬C1 | D1 u D2 | 9R.{a} | 8R.D1 | 6 nR.C1 | 6 nR.>
133
L. Bozzato, T. Eiter, L. Serafini. Defeasibility in contextual reasoning with CKR
where A is a concept name, R is role name and n 2 {0, 1}. A both-side concept E, F
is a concept expression which is both a left- and right-side concept. TBox axioms can
only take the form C v D or E ⌘ F . The RBox for SROIQ-RL can contain every
role axiom of SROIQ except for Ref(R). ABox concept assertions can be only stated
in the form D(a), where D is a right-side concept.
3 CKR with defeasible axioms
We now introduce CKRs and extend them with primitives to express defeasible axioms.
We first present the syntax and then define a model-based semantics for the interpreta-
tion of defeasible inheritance from the upper contexts.
A Contextualized Knowledge Repository (CKR) is a two layered structure. The up-
per layer consists of a knowledge base G, which describes two types of knowledge: (i)
the structure and the properties of contexts of the CKR (called meta-knowledge), and
(ii) the knowledge that is context independent, i.e., that holds in every context (called
global knowledge). The lower layer is constituted by a set of (local) contexts; each
contains (locally valid) facts and can also refer to what holds in other contexts.
Meta-Language. The meta-knowledge of a CKR is expressed by a DL language de-
fined on a meta-vocabulary, containing the elements that define the contextual structure.
Definition 1 (Meta-vocabulary). A meta-vocabulary is a DL vocabulary composed
of a set NC of atomic concepts, a set NR of atomic roles, and a set NI of individual
constants that are mutually disjoint and contain the following sets of symbols
1. N ✓ NI of context names. 4. R ✓ NR of contextual relations.
2. M ✓ NI of module names. 5. A ✓ NR of contextual attributes.
3. C ✓ NC of context classes, 6. For every attribute A 2 A, a set
including the class Ctx. DA ✓ NI of attribute values of A.
We use the role mod 2 NR defined on N⇥M to express associations between contexts
and modules. The meta-language L of a CKR is a DL language over with the
following syntactic conditions on the application of role restrictions: for every • 2
{8, 9, 6 n, > n}, (i) for a concept •A.B, then B is in the form B = {a} with a 2 DA ;
(ii) for a concept •mod.B, then B is in the form B = {m} with m 2 M.
Object Language. The context (in)dependent knowledge of a CKR is expressed via
a DL language called object-language L⌃ over an object-vocabulary ⌃ = NC⌃ ]
NR⌃ ] NI⌃ . Expression in L⌃ will be evaluated locally to each context, i.e., each
context can interpret each symbol independently. However, sometimes one wants to
constrain the meaning of a symbol in a context with the meaning of a symbol in some
other context. For such external references, we extend the object language L⌃ to Le⌃
with eval expressions of the form eval(X, C), where X is a concept or role expression
of L⌃ and C is a concept expression of L (with C v Ctx).
Defeasible Axioms. Compared to [4], we extend the types of axioms that can appear
in the global object knowledge G with defeasible axioms. Given an axiom ↵ 2 L⌃ , the
assertion D(↵) in G states that ↵ is a defeasible axiom of G. Intuitively, this statement
means that ↵, at the level of instantiations for individuals, propagates to a local context
unless it is contradicted there, and thus an exception to ↵ for individuals is tolerated.
134
L. Bozzato, T. Eiter, L. Serafini. Defeasibility in contextual reasoning with CKR
Example 1. A defeasible fact D(Expensive(concert)) might express that a concert is
expensive and propagate this to local contexts. At such a context, this might be con-
tradicted by an assertion ¬Expensive(concert), which then overrides the global asser-
tion. Likewise, such overriding should take place if we have a global axiom Cheap v
¬Expensive and a local assertion Cheap(concert), such that ¬Expensive(concert)
can be derived at the local context. 3
Example 2. Beyond facts, from a defeasible GCI axiom D(Cheap v Interesting)
(“cheap events are interesting”) and the global assertion Cheap(fbmatch) (“football
matches are cheap”), we may conclude Interesting(fbmatch) at a local context; how-
ever, an assertion ¬Interesting(fbmatch) there would contradict this and should over-
ride the instance of the defeasible axiom for fbmatch: that is, the fact ¬Cheap t
Interesting(fbmatch) may be violated. 3
The DL language LD
⌃ extends L⌃ with the set of defeasible axioms in L⌃ .
CKR Syntax. We are now ready to give our formal definition of Contextualized
Knowledge Repository.
Definition 2 (Contextualized Knowledge Repository, CKR). A Contextualized Knowl-
edge Repository (CKR) over a meta-vocabulary and an object vocabulary ⌃ is a
structure K = hG, {Km }m2M i where:
– G is a DL knowledge base over L [ LD ⌃ , and
– every Km is a DL knowledge base over Le⌃ , for each module name m 2 M.
In particular, K is a SROIQ-RL CKR, if G and all Km are knowledge bases over
the extended language of SROIQ-RL where eval-expressions can only occur in left-
concepts and contain left-concepts or roles. In the following, we tacitly focus on such
CKR. We show how the examples in the introduction can be formalized as CKRs.
Example 3. In the first example (inspired by a real application of CKR3 ) we want to
define an event recommendation system: we thus represent touristic events and prefer-
ences of tourists in order to be able to derive appropriate suggestions. In particular, we
want to assert that, in general, all of the Cheap events are Interesting; we do so by
expressing this as a defeasible axiom in the global context. Furthermore, we propose
local markets (market) and football matches (fbmatch) as examples of cheap events.
On the other hand, we want to reflect that tourists interested in cultural events are not
interested in a sportive event like a football match4 ; we express this by negating the
interest in f bmatch. Thus, our example CKR Ktour = hG, {Kctourist m }i has:
G : { D(Cheap v Interesting), Cheap(fbmatch), Cheap(market),
mod(cultural tourist, ctourist m) },
Kctourist m : { ¬Interesting(fbmatch) }.
Note that the negative assertion in the local context represents, as discussed in Exam-
ple 2, an exception to the defeasible axiom: we want to recognize this “overriding” for
the fbmatch instance, but still apply the defeasible inclusion for market. 3
3
http://www.investintrentino.it/News/Trentour-Trentino-
platform-for-smart-tourism
4
To keep things simple, we omit modeling sportive events by a separate concept.
135
L. Bozzato, T. Eiter, L. Serafini. Defeasibility in contextual reasoning with CKR
Example 4. Our next example shows how we can represent a form of defeasible prop-
agation of information across local contexts using eval expressions. We want to rep-
resent the information about an organization in a CKR, using contexts to represent its
situation in different years. We express the rule that every employee working the years
before (WorkingBefore) also works in the current year (WorkingNow ) by a defeasible
inclusion. In the module associated to 2012, we say that alice, bob and charlie were
working last year. In the module for 2013, we say (using an eval expression) that all of
the employees working in 2012 have to be considered in the set of employees working
in the past years; moreover, we say that charlie no longer works for the organization.
This can be encoded in the CKR Korg = hG, {Kem2012 m , Kem2013 m }i, where
⇢
D(WorkingBefore v WorkingNow ),
G:
mod(employees2012, em2012 m), mod(employees2013, em2013 m)
Kem2012 m : { WorkingNow (alice), WorkingNow (bob), WorkingNow (charlie) }
⇢
eval(WorkingNow , {employees2012}) v WorkingBefore,
Kem2013 m :
¬WorkingNow (charlie)
Intuitively, at the local context employees2013, where WorkingBefore(charlie) can be
derived, the negative assertion ¬WorkingNow (charlie) should override the instance of
the inclusion axiom in the global context for charlie, as it would lead to the opposite,
i.e., WorkingNow (charlie); on the other hand, for alice and bob no overriding should
happen and we can derive that they still work for the organization. 3
Semantics. We now define a model-based semantics for CKRs. The idea is to model
exceptions of axiom instances by so called clashing assumptions, which are pairs h↵, ei
of an axiom and a set of individuals, to the effect that in the evaluation at the local
context, the instance of ↵ for e is disregarded. However, such a clashing assumption
must be justified, in the sense that the instance of ↵ for e must be unsatisfiable at the
local context. This is ensured if there are assertions that can be derived which prove this
unsatisfiability: we call such assertions clashing sets. Models of a CKR will be then
CKR interpretations in [4] extended with clashing assumptions that are all justified.
Definition 3 (CKR interpretation). A CKR interpretation for h , ⌃i is a structure
I = hM, Ii s.t.
– M is a DL interpretation of [ ⌃ s.t., for every c 2 N, cM 2 CtxM and, for every
C 2 C, CM ✓ CtxM ;
– for every x 2 CtxM , I(x) is a DL interpretation over ⌃ s.t. I(x) = M and, for
a 2 NI⌃ , aI(x) = aM .
The interpretation of ordinary DL expressions on M and I(x) in I = hM, Ii is as
usual; eval expressions are interpreted as follows: for every x 2 CtxM ,
S
eval(X, C)I(x) = e2CM X I(e)
According to the previous definition, a CKR interpretation consists of an interpretation
for the “upper-layer” (which includes the global knowledge and the meta-knowledge)
and an interpretation of the object language for each instance of type context (i.e., for
all x 2 CtxM ), providing a semantics of the object-vocabulary in x.
136
L. Bozzato, T. Eiter, L. Serafini. Defeasibility in contextual reasoning with CKR
An instantiation of an axiom ↵ 2 L⌃ with a tuple e of individuals in NI⌃ , written
↵(e), is the specialization of ↵, viewed as its first order translation in an universal
sentence 8x. ↵ (x), to e (i.e., ↵ (e)); accordingly, e.g., e is void for assertions, a single
element e for GCIs, and a pair e1 , e2 of elements for role axioms.
A clashing assumption is pair h↵, ei such that ↵(e) is an axiom instantiation; intu-
itively, it represents the assumption that ↵(e) is not (DL-)satisfiable. A clashing set for
a h↵, ei is a satisfiable set S of ABox assertions such that S [ {↵(e)} is unsatisfiable.
That is, S provides an assertional “justification” for the assumption of local overriding
of ↵ on e.
Given a CKR interpretation I = hM, Ii, we call the structure ICAS = hM, I, CAS i
a CAS -interpretation, where CAS is a map such that, for every x 2 M , CAS (x) is
a set of clashing assumptions for x.
Definition 4 (CAS -model). Given a CKR K = hG, {Km }m2M i and a CAS -interpretation
ICAS = hM, I, CAS i, we say that ICAS is a CAS -model for K (ICAS |= K) if
– for every ↵ 2 L⌃ [ L in G, M |= ↵;
– for every D(↵) 2 G with ↵ 2 L⌃ , M |= ↵;
– if hx, yi 2 modM and y = mM , then I(x) |= Km ;
– for every ↵ 2 G \ L⌃ and x 2 CtxM , I(x) |= ↵, and
– for every D(↵) 2 G with ↵ 2 L⌃ , x 2 CtxM , and domain elements d ✓ I(x)
, if
d 6= eM for every h↵, ei 2 CAS (x), then I(x) |= ↵(d).
For ↵ 2 Le⌃ and c 2 N, we write K |=CAS c : ↵ if for every CAS -interpretation ICAS
it holds that ICAS |= K implies I(cM ) |= ↵; for ↵ 2 L , we write K |=CAS ↵ if for
every CAS -interpretation ICAS it holds that ICAS |= K implies M |= ↵.
We say that a CAS -model ICAS = hM, I, CAS i of K is justified if, for every x 2
CtxM and h↵, ei 2 CAS (x), some clashing set Sx,h↵,ei exists such that for every CAS -
0
model I0CAS = hM0 , I 0 , CAS i of K with M = M , it holds I 0 (x) |= Sx,h↵,ei .
Informally, justification requires that we have factual evidence that an instantiation of
an axiom can not be satisfied, and this evidence is provable. Based on this, we now give
the definition of CKR model:
Definition 5 (CKR model). A CKR interpretation I = hM, Ii is a CKR model of K
(in symbols, I |= K), if some ICAS = hM, I, CAS i is a justified CAS -model for K.
For ↵ 2 Le⌃ and c 2 N, we write K |= c : ↵ if I(cM ) |= ↵ for every CKR model I of
K; similarly for ↵ 2 L , we write K |= ↵ if M |= ↵ for every CKR model I of K.
We can show the following properties:
Proposition 1. Suppose that I = hM, Ii and I0 = hM0 , I 0 i are CKR models of K
such that ICAS = hM, I, CAS i and I0CAS 0 = hM0 , I 0 , CAS 0 i are justified CAS -
0
models of K. Then CtxM = CtxM and CAS 0 (x) ✓ CAS (x) for every x 2 CtxM
implies CAS = CAS 0 .
The previous result shows that, given the justification of the CKR model, there is a
notion of minimality on the sets of clashing assumptions related to each context.
Given a CAS -interpretation ICAS = hM, I, CAS i, we denote with IN CAS =
0
hM0 , I 0 , CAS 0 i the interpretation in which: (i) M = {aM | a 2 NI [ NI⌃ };
0
(ii) M0 , I 0 and CAS 0 are the restrictions of M, I and CAS to M , respectively.
137
L. Bozzato, T. Eiter, L. Serafini. Defeasibility in contextual reasoning with CKR
Proposition 2. Let ICAS be a justified CAS -model of K. Then, also the CAS -interpre-
tation IN
CAS is a justified CAS -model of K.
Basically, the result shows that justification for a CKR only depends on the “named
contexts” part of the considered CAS -model: intuitively, this allow us to consider such
restricted models in the correctness result of the datalog translation presented in the
following section.
Example 5. We can now show an example of CKR models satisfying the example
CKRs presented in Example 3.
In the case of Ktour , we can consider a model ICAS tour = hM, I, CAS tour i such
that CAS tour (cultural touristM ) = {hCheap v Interesting, {f bmatch}i}. Note
that the interpretation is justified as it is easy to check that Ktour |= cultural tourist :
{Cheap(fbmatch), ¬Interesting(fbmatch)}, that represents a clashing set for the de-
feasible axiom. Moreover, for the definition of satisfiability under the assumptions in
CAS tour , we obtain that I(cultural touristM ) |= Interesting(market).
Similarly, for Korg , we have that the model ICAS org = hM, I, CAS org i with
CAS org (employees2013M ) = {hWorkingBefore v WorkingNow , {charlie}i} is a
CKR model for the example CKR. For the interpretation of eval expressions, in every in-
terpretation of Korg we have that {alice I(x) , bob I(x) , charlie I(x) } v WorkingBefore I(x) ,
where x = employees2013. Thus the justification of the model can be easily seen as
Korg |= employees2013 : S for S = {WorkingBefore(charlie), ¬WorkingNow (charlie)},
which represents a clashing set for the defeasible axiom on charlie. On the other hand,
for the satisfiability under the assumptions in CAS org , we obtain that I(employeesM ) |=
WorkingNow (alice) and I(employeesM ) |= WorkingNow (bob). 3
As clashing assumptions in CAS maps are ground instances of axioms, they refer
merely to named individuals. We remark that using standard names for the domain
elements, one could permit clashing assumptions for all elements; the results in Propo-
sitions 1 and 2 carry over to this setting.
4 CKR translation to general programs
We revise the datalog translation for SROIQ-RL CKR from [4] with rules for the
detection of axiom overriding and defeasible propagation of global knowledge. To sim-
plify the presentation of rules, we introduce a normal form for the considered axioms.
We say that a CKR K = hG, {Km }m2M i is in normal form if:
– G contains axioms in L of the form of Table 1 or in the form C v 9mod.{m},
C v 9A.{dA } for A, B, C 2 C, R, S, T 2 R, a, b 2 N, m 2 M, A 2 A and dA 2 DA .
– G and every Km contain axioms in L⌃ of the form of Table 1 and every Km contain
axioms in Le⌃ of the form eval(A, C) v B, eval(R, C) v T for A, B, C 2 NC⌃ ,
a, b 2 NI⌃ , R, S, T 2 NR⌃ and C 2 C.
– G contains defeasible axioms D(↵) 2 LD ⌃ with ↵ of the form of Table 1.
It can be seen that for named interpretations, i.e., of the form IN
CAS , every CKR can be
rewritten into an equivalent one in normal form (using new symbols).
138
L. Bozzato, T. Eiter, L. Serafini. Defeasibility in contextual reasoning with CKR
A(a) R(a, b) ¬A(b) ¬R(a, b) a=b a 6= b
AvB {a} v B A v ¬B AuB vC
9R.A v B A v 9R.{a} A v 8R.B A v 61R.B
RvT R SvT Dis(R, S) Inv(R, S) Irr(R)
Table 1. Normal form axioms
In this version of the translation, the definition of program has now to be adapted to
the new form of the rules (admitting negative literals) and to the answer set semantics
of the resulting logic program.
Syntax. A signature is a tuple hC, Pi of a finite set C of constants and a finite set P of
predicates. We assume a set V of variables; the elements of C [ V are terms. An atom
is of the form p(t1 , . . . , tn ) where p 2 P and t1 , . . . , tn , are terms. A literal l is either
a positive literal p or a negative literal ¬p with p an atom and ¬ the symbol of strong
negation. Literals of the form p, ¬p are complementary.
A rule r is an expression of the form
a b1 , . . . , bk , not bk+1 , . . . , not bm .
where a, b1 , . . . , bm are literals and not is the negation as failure symbol (NAF). We
denote with Head(r) the head a of rule r and with Body + (r) and Body (r) the pos-
itive (b1 , . . . , bk ) and NAF (bk+1 , . . . , bm ) part of the body of the rule5 . A fact H is a
ground rule with empty body (we then omit ). A program P is a finite set of rules. A
ground substitution for hC, Pi is a function : V ! C; (ground) substitutions on
atoms and ground instances of atoms are as usual.
Semantics. Given a program P , we define the universe UP of P as the set of all con-
stants occurring in P and the base BP of P as the set of all the ground literals con-
structible from the predicates in P and the constants in UP . An interpretation I ✓ BP
is a consistent subset of BP (i.e., not containing complementary literals). We say that a
literal l is true in I iff l 2 I and false otherwise.
Given a rule r 2 ground(P ), the body of r is true in I if: (1) every literal in
Body + (r) is true w.r.t. I, and (2) every literal in Body (r) is false w.r.t. I. A rule r is
satisfied in I if either the head of r is true in I or the body of r is not true in I.
An interpretation I for P is a model for P (I |= P ), if every rule in ground(P ) is
satisfied in I; it is a minimal model for P , if no proper subset I 0 ⇢ I is a model for P .
Given an interpretation I for P , the (Gelfond-Lifschitz) reduct of P w.r.t. I, denoted
by GI (P ), is the set of rules obtained from ground(P ) by (i) removing every rule
r such that Body (r) \ I 6= ;. (ii) removing the NAF part from the bodies of the
remaining rules. Then I is an answer set of P , if I is a minimal model of the positive
version pos(GI (P )) of GI (P ) (i.e. the positive program obtained by considering each
negative literal ¬p(t1 , . . . , tn ) as a positive one with predicate symbol ¬p).
The following property is well-known.
Lemma 1. If M is an answer set for P , then M is a minimal model of P .
5
In the rules, we might write (¬)p to denote that the rule holds both for the positive and negative
literal associated to p. This will be used only as a shortcut to simplify the presentation of rules.
139
L. Bozzato, T. Eiter, L. Serafini. Defeasibility in contextual reasoning with CKR
Using this interpretation for our programs, we say that a literal H 2 BP is a con-
sequence of P and we write P |= H iff for every answer set M of P we have that
M |= H.
Translation. We now are ready to present our translation. As in [4], we basically in-
stantiate and adapt the materialization calculus in [10] to meet the structure of CKR.
The translation is composed by the following sets: the input translations Iglob , Iloc ,
ID , Irl , the deduction rules Ploc , PD , Prl , and output translation O, such that:
– every input translation I and output translation O are partial functions (defined over
axioms in normal form) while deduction rules P are sets of datalog rules;
– given an axiom or signature symbol ↵ (and c 2 N), each I(↵) (or I(↵, c)) is either
undefined or a set of datalog facts or rules;
– given an axiom ↵ and c 2 N, O(↵, c) is either undefined or a single datalog fact;
We extend the definition of inputStranslations to
Sknowledge bases (set of axioms) S with
their signature ⌃, with I(S) = ↵2S I(↵) [ s2⌃,I(s) defined I(s) (similarly I(S, c) =
S S
↵2S I(↵, c) [ s2⌃,I(s) defined I(s, c)).
We briefly present the form of the different sets of translation and deduction rules
involved in the translation process: the tables containing the complete set of rules can
be found in the Appendix.
The set of rules in Irl (S, c) define the rules to translate SROIQ-RL axioms and
signature: for example, we have the following rule for concept inclusions: A v B 7!
{subClass(A, B, c)}. The set of rules Prl are the corresponding deduction rules for
axioms in SROIQ-RL: for example, for atomic concept inclusions we have the rule:
instd(x, z, c) subClass(y, z, c), instd(x, y, c).
Global input rules of Iglob (G), basically encode the interpretation of Ctx in the global
context. Similarly, local input rules Iloc (Km , c) and local deduction rules Ploc provide
the translation and rules for elements of the local object language, in particular for eval
expression: e.g., for inclusion of concepts with a left eval expression we have the input
rule eval(A, C) v B 7! {subEval(A, C, B, c)} and the corresponding deduction rule
instd(x, b, c) subEval(a, c1 , b, c), instd(c0 , c1 , gm), instd(x, a, c0 ).
The input rules in ID provide the translation of defeasible axioms in the global context:
given a defeasible axiom D(↵), Irl (↵, gk) is applied and a rule defining when the axiom
is locally overridden is added to the program. For example, if D(A v B) 2 G, the fact
subClass(A, B, gk). is added to the program for the global context together with the
corresponding overriding rule:
ovr(subClass, x, A, B, c) ¬instd(x, B, c), instd(x, A, c), prec(c, g).
The deduction rules in PD , on the other hand, provide the definition of the defeasible
propagation of axioms from the global context to the local contexts. For example, the
following rule propagates an atomic concept inclusion axiom: if the inclusion axiom is
in the program of the global context and can be applied to a local instance, it is applied
only if the instance is not recognized as an exception:
140
L. Bozzato, T. Eiter, L. Serafini. Defeasibility in contextual reasoning with CKR
instd(x, z, c) subClass(y, z, g), instd(x, y, c),
prec(c, g), not ovr(subClass, x, y, z, c).
Finally, the set of output rules O(↵, c) provides the translation of ABox assertions that
can be verified by applying the rules of the final program. For example, the case for
atomic concept assertions in a given context c is given as A(a) 7! {instd(a, A, c)}.
Given a CKR K = hG, {Km }m2M i, the translation to its datalog program follows
these steps:
1. the global program for G is translated to (where gm, gk are new context names):
P G(G) = Iglob (G ) [ ID (G ) [ Irl (G , gm) [ Irl (G⌃ , gk) [ Prl
where G = {↵ 2 G | ↵ 2 L } and G⌃ = {↵ 2 G | ↵ 2 LD
⌃ }.
2. We define the set of contexts:
NG = {c 2 N | P G(G) |= instd(c, Ctx, gm)}
For every c 2 NG , we define its associated knowledge base as:
[
Kc = {Km 2 K | P G(G) |= tripled(c, mod, m, gm)}
3. We define each local program for c 2 NG as:
P C(c) := Ploc [ PD [ Iloc (Kc , c) [ Irl (Kc , c) [ {prec(c, gk).}
4. The CKR program is then defined as:
S
P K(K) = P G(G) [ c2NG P C(c)
We say that G entails an axiom ↵ 2 L (denoted G |= P
↵) if P G(G) and O(↵, gm)
are defined and P G(G) |= O(↵, gm). Similarly, G entails an axiom ↵ 2 L⌃ (denoted
G |=
P
↵) if P G(G) and O(↵, gk) are defined and P G(G) |= O(↵, gk). We say that K
entails an axiom ↵ 2 Le⌃ in a context c 2 N (denoted K |=P
c : ↵), if the elements of
P K(K) and O(↵, c) are defined and P K(K) |= O(↵, c).
Correctness of the translation. In the following we show the correctness of the trans-
lation with respect to the problem of instance checking in the presented semantics for
CKR. Let CAS N be a map associating every c 2 N to a set CAS N (c) of clashing
assumptions. We define the set of the corresponding overriding assumptions:
OVR(CAS N ) = {ovr(p(e)) | h↵, ei 2 CAS N (c), Irl (↵, c) = p}
Given a CKR K and its associated CKR program P K(K), the OVR-reduct of P K(K)
(denoted by GOVR (P K(K))) is the set of rules obtained from ground(P K(K)) by: (i)
removing every rule r such that B (r) \ OVR(CAS N ) 6= ;; (ii) removing the NAF
part (which involves only instances of ovr) from the bodies of the remaining rules.
Consider a CKR interpretation I = hM, Ii and CAS M M M
N such that CAS N (c ) =
CAS N (c), for all c 2 N. We can show that the following property holds:
141
L. Bozzato, T. Eiter, L. Serafini. Defeasibility in contextual reasoning with CKR
Lemma 2. GOVR (P K(K)) |= O(↵, c) iff K |=CASNM c : ↵ (if O(↵, c) is defined).
We can prove the lemma by establishing the following propositions
Proposition 3 (cf. [4]). For every ↵, ground(P G(G)) |= O(↵, g) iff G |= ↵.
Proposition 4. For every ↵ (s.t. O(↵, c) is defined),
1. (CAS -soundness) If GOVR (P K(K)) |= O(↵, c), then K |=CASNM c : ↵.
2. (CAS -completeness) If K |=CASNM c : ↵, then GOVR (P K(K)) |= O(↵, c).
The completeness of the translation procedure with respect to CKR semantics can be
proved using the following results. Let S|p be the restriction of an answer set S to the
set of facts for predicate p.
Lemma 3. For every justified CAS -model ICAS M N
= hM, I, CASNM i of K, some an-
swer set S of P K(K) exists such that S|ovr = OVR(CAS N ).
Lemma 4. For every answer set S of P K(K), some justified CAS -model ICAS M S
=
hM, I, CASSM i of K exists such that CAS S (c) = {h↵, ei | Irl (↵, c) = p, ovr(p(e)) 2
S} for every c 2 N.
The correctness result directly follows from previous results.
Theorem 1. For a normal form CKR K, K |= c : ↵ iff P K(K) |= O(↵, c) (provided
O(↵, c) is not void).
5 Conclusion
We presented an extension to the Contextualized Knowledge Repository (CKR) frame-
work introducing a notion of defeasibility of axioms across contexts. We then presented
a datalog translation for the extended semantics, based on the materialization calculus
for instance checking in [4]. In the translation, non-monotonicity is expressed using an-
swer set semantics, such that instance checking over OWL RL based CKR reduces to
cautious inference from all answer sets of the translation.
An implementation of the presented translation in a prototype is ongoing. It basi-
cally builds on the DReW DL datalog rewriter [16], and extends the basic translation of
OWL RL ontologies to the two layered structure of CKR. Given as input an ontology
representing the global context and ontologies representing the knowledge modules, the
translation produces a datalog program (compliant to DLV syntax) representing the in-
put CKR. More specifically, it encodes the rules and the two layered translation process
presented in Section 4: after the translation of the global context, the set of contexts and
their associations to modules are derived from the global program through interaction
with the DLV solver; with the local knowledge bases defined, the programs for the lo-
cal contexts are then computed. We aim at extending the current prototype to access
external data sources; moreover, we want to compare the query performance with the
available implementation of CKR based on SPARQL forward rules [4].
142
L. Bozzato, T. Eiter, L. Serafini. Defeasibility in contextual reasoning with CKR
An interesting direction for future investigation is the comparison of the proposed
approach to the known approaches to integrate notions of defeasibility and defaults
in description logics. Notable examples of such approaches include representations of
typicality in DLs concepts [6] and works employing circumscription in description log-
ics [1]. It is interesting to see whether such notions of defeasibility can be reduced to
our representation, thus leading to an implementation of such approaches.
Another natural continuation to the presented work is to allow defeasible axioms
across local contexts, possibly along an explicit order relation between contexts (as the
coverage relation [12]), or across knowledge modules, allowing overriding in specific
instances of context classes associated to such modules.
Acknowledgments. The research leading to these results has received funding from
the European Union’s Seventh Framework Programme (FP7/2007-2013) under grant
agreement no.257641 (PlanetData NoE).
References
1. Bonatti, P.A., Lutz, C., Wolter, F.: Description logics with circumscription. In: KR. pp. 400–
410 (2006)
2. Bozzato, L., Ghidini, C., Serafini, L.: Comparing contextual and flat representations of
knowledge: a concrete case about football data. In: K-CAP 2013. pp. 9–16. ACM (2013)
3. Bozzato, L., Homola, M., Serafini, L.: Towards More Effective Tableaux Reasoning for CKR.
In: DL2012. CEUR-WP, vol. 824, pp. 114–124. CEUR-WS.org (2012)
4. Bozzato, L., Serafini, L.: Materialization Calculus for Contexts in the Semantic Web. In:
DL2013. CEUR-WP, vol. 1014. CEUR-WS.org (2013)
5. Buccafurri, F., Faber, W., Leone, N.: Disjunctive logic programs with inheritance. In: ICLP.
pp. 79–93 (1999)
6. Giordano, L., Gliozzi, V., Olivetti, N., Pozzato, G.L.: A non-monotonic description logic for
reasoning about typicality. Artif. Intell. 195, 165–202 (2013)
7. Khriyenko, O., Terziyan, V.: A framework for context sensitive metadata description. IJSMO
1(2), 154–164 (2006)
8. Klarman, S., Gutiérrez-Basulto, V.: ALC ALC : a context description logic. In: JELIA (2010)
9. Klarman, S.: Reasoning with Contexts in Description Logics. Ph.D. thesis, Free University
of Amsterdam (2013)
10. Krötzsch, M.: Efficient Inferencing for OWL EL. In: JELIA 2010. Lecture Notes in Com-
puter Science, vol. 6341, pp. 234–246. Springer (2010)
11. Motik, B., Fokoue, A., Horrocks, I., Wu, Z., Lutz, C., Grau, B.C.: OWL 2 Web Ontology Lan-
guage Profiles. W3C recommendation, W3C (Oct 2009), http://www.w3.org/TR/2009/REC-
owl2-profiles-20091027/
12. Serafini, L., Homola, M.: Contextualized knowledge repositories for the semantic web. J. of
Web Semantics 12 (2012)
13. Straccia, U., Lopes, N., Lukácsy, G., Polleres, A.: A general framework for representing and
reasoning with annotated semantic web data. In: AAAI 2010. AAAI Press (2010)
14. Tanca, L.: Context-Based Data Tailoring for Mobile Users. In: BTW 2007 Workshops. pp.
282–295 (2007)
15. Udrea, O., Recupero, D., Subrahmanian, V.S.: Annotated RDF. ACM Trans. Comput. Log.
11(2), 1–41 (2010)
16. Xiao, G., Heymans, S., Eiter, T.: DReW: a reasoner for datalog-rewritable description logics
and dl-programs. In: BuRO 2010 (2010)
143
L. Bozzato, T. Eiter, L. Serafini. Defeasibility in contextual reasoning with CKR
A Appendix: rules tables
Global input rules Iglob (G)
(igl-subctx1) C 2 C 7! {subClass(C, Ctx, gm)}
(igl-subctx2) c 2 N 7! {insta(c, Ctx, gm)}
Local input rules Iloc (Km , c)
(ilc-subevalat) eval(A, C) v B 7! {subEval(A, C, B, c)}
(ilc-subevalr) eval(R, C) v T 7! {subEvalR(R, C, T, c)}
Local deduction rules Ploc
(plc-subevalat) instd(x, b, c) subEval(a, c1 , b, c), instd(c0 , c1 , gm), instd(x, a, c0 ).
(plc-subevalr) tripled(x, t, y, c) subEvalR(r, c1 , t, c), instd(c0 , c1 , gm), tripled(x, r, y, c0 ).
(plc-eq) eq(x, y, c) nom(x, c), eq(x, y, c0 ).
Output translation O(↵, c)
(o-concept) A(a) 7! {instd(a, A, c)}
(o-role) R(a, b) 7! {tripled(a, R, b, c)}
(o-nconcept) ¬A(a) 7! {¬instd(a, A, c)}
(o-nrole) ¬R(a, b) 7! {¬tripled(a, R, b, c)}
Table 2. Global, local and output rules
For D(↵) 2 S, apply Irl (↵) and the corresponding rule in the following:
(ovr-inst1) D(A(a)) 7! { ovr(insta, a, A, c) ¬instd(a, A, c), prec(c, g). }
(ovr-inst2) D(¬A(a)) 7! { ovr(¬insta, a, A, c) instd(a, A, c), prec(c, g). }
(ovr-triple1) D(R(a, b)) 7! { ovr(triplea, a, R, b, c) ¬tripled(a, R, b, c), prec(c, g). }
(ovr-triple2) D(¬R(a, b)) 7! { ovr(¬triplea, a, R, b, c) tripled(a, R, b, c), prec(c, g). }
(ovr-inst3) D({a} v B) 7! { ovr(insta, a, B, c) ¬instd(a, B, c), prec(c, g). }
(ovr-subc) D(A v B) 7! { ovr(subClass, x, A, B, c) ¬instd(x, B, c), instd(x, A, c), prec(c, g). }
(ovr-not) D(A v ¬B) 7! { ovr(supNot, x, A, B, c) instd(x, B, c), instd(x, A, c), prec(c, g). }
(ovr-cnj) D(A1 u A2 v B) 7! { ovr(subConj, x, A1 , A2 , B, c)
¬instd(x, B, c), instd(x, A1 , c), instd(x, A2 , c), prec(c, g). }
(ovr-subex) D(9R.A v B) 7! { ovr(subEx, x, R, A, B, c)
¬instd(x, B, c), tripled(x, R, y, c), instd(y, A, c), prec(c, g). }
(ovr-supex) D(A v 9R.{a}) 7! { ovr(supEx, x, A, R, a, c)
¬tripled(x, R, a, c), instd(x, A, c), prec(c, g). }
(ovr-forall) D(A v 8R.B) 7! { ovr(supForall, x, y, A, R, B, c)
¬instd(y, B, c), instd(x, A, c), tripled(x, R, y, c), prec(c, g). }
(ovr-leqone) D(A v6 1R.B) 7! { ovr(supLeqOne, x, y, z, A, R, B, c)
¬eq(z, y, c), instd(x, A, c), tripled(x, R, y, c), tripled(x, R, z, c),
instd(y, B, c), instd(z, B, c), prec(c, g). }
(ovr-subr) D(R v S) 7! { ovr(subRole, x, y, R, S, c)
¬tripled(x, S, y, c), tripled(x, R, y, c), prec(c, g). }
(ovr-subrc) D(R S v T ) 7! { ovr(subRChain, x, y, z, R, S, T, c)
¬tripled(x, T, z, c), tripled(x, R, y, c), tripled(y, S, z, c), prec(c, g). }
(ovr-dis) D(Dis(R, S)) 7! { ovr(dis, x, y, R, S, c)
tripled(x, S, y, c), tripled(x, R, y, c), prec(c, g). }
(ovr-inv) D(Inv(R, S)) 7! { ovr(inv, x, y, R, S, c)
¬tripled(x, S, y, c), tripled(x, R, y, c), prec(c, g).
ovr(inv, x, y, R, S, c)
¬tripled(x, R, y, c), tripled(x, S, y, c), prec(c, g). }
(ovr-irr) D(Irr(R)) 7! { ovr(irr, x, R, c) tripled(x, R, x, c), prec(c, g). }
Table 3. Input rules ID (S) for defeasible axioms
144
L. Bozzato, T. Eiter, L. Serafini. Defeasibility in contextual reasoning with CKR
(prop-inst) (¬)instd(x, z, c) (¬)insta(x, z, g), prec(c, g), not ovr((¬)insta, x, z, c).
(prop-triple) (¬)tripled(x, r, y, c) (¬)triplea(x, r, y, g), prec(c, g), not ovr((¬)triplea, x, r, y, c).
(prop-subc) instd(x, z, c) subClass(y, z, g), instd(x, y, c), prec(c, g), not ovr(subClass, x, y, z, c).
(prop-not) ¬instd(x, z, c) supNot(y, z, g), instd(x, y, c), prec(c, g), not ovr(supNot, x, y, z, c).
(prop-cnj) instd(x, z, c) subConj(y1 , y2 , z, g), instd(x, y1 , c), instd(x, y2 , c),
prec(c, g), not ovr(subConj, x, y1 , y2 , z, c).
(prop-subex) instd(x, z, c) subEx(v, y, z, g), tripled(x, v, x0 , c), instd(x0 , y, c),
prec(c, g), not ovr(subEx, x, v, y, z, c).
(prop-supex) tripled(x, r, x0 , c) supEx(y, r, x0 , g), instd(x, y, c),
prec(c, g), not ovr(supEx, x, y, r, x0 , c).
(prop-forall) instd(y, z 0 , c) supForall(z, r, z 0 , g), instd(x, z, c), tripled(x, r, y, c),
prec(c, g), not ovr(supForall, x, y, z, r, z 0 , c).
(prop-leqone) eq(x1 , x2 , c) supLeqOne(z, r, z 0 , g), instd(x, z, c), tripled(x, r, x1 , c),
instd(x1 , z 0 , c), tripled(x, r, x2 , c), instd(x2 , z 0 , c),
prec(c, g), not ovr(supLeqOne, x, x1 , x2 , z, r, z 0 , c).
(prop-subr) tripled(x, w, x0 , c) subRole(v, w, g), tripled(x, v, x0 , c),
prec(c, g), not ovr(subRole, x, y, v, w, c).
(prop-subrc) tripled(x, w, z, c) subRChain(u, v, w, g), tripled(x, u, y, c), tripled(y, v, z, c),
prec(c, g), not ovr(subRChain, x, y, z, u, v, w, c).
(prop-dis1) ¬tripled(x, v, y, c) dis(u, v, g), tripled(x, u, y, c),
prec(c, g), not ovr(dis, x, y, u, v, c).
(prop-dis2) ¬tripled(x, u, y, c) dis(u, v, g), tripled(x, v, y, c),
prec(c, g), not ovr(dis, x, y, u, v, c).
(prop-inv1) tripled(y, v, x, c) inv(u, v, g), tripled(x, u, y, c),
prec(c, g), not ovr(inv, x, y, u, v, c).
(prop-inv2) tripled(y, u, x, c) inv(u, v, g), tripled(x, v, y, c),
prec(c, g), not ovr(inv, x, y, u, v, c).
(prop-irr) ¬tripled(x, u, x, c) irr(u, g), nom(x, c),
prec(c, g), not ovr(irr, x, u, c).
Table 4. Deduction rules PD for defeasible axioms
145
L. Bozzato, T. Eiter, L. Serafini. Defeasibility in contextual reasoning with CKR
RL input translation Irl (S, c)
(irl-nom) a 2 NI 7! {nom(a, c)} (irl-not) A v ¬B 7! {supNot(A, B, c)}
(irl-cls) A 2 NC 7! {cls(A, c)} (irl-subcnj) A1 u A2 v B 7! {subConj(A1 , A2 , B, c)}
(irl-rol) R 2 NR 7! {rol(R, c)} (irl-subex) 9R.A v B 7! {subEx(R, A, B, c)}
(irl-inst1) A(a) 7! {insta(a, A, c)} (irl-supex) A v 9R.{a} 7! {supEx(A, R, a, c)}
(irl-inst2) ¬A(a) 7! {¬insta(a, A, c)} (irl-forall) A v 8R.B 7! {supForall(A, R, B, c)}
(irl-triple) R(a, b) 7! {triplea(a, R, b, c)} (irl-leqone) A v 61R.B 7! {supLeqOne(A, R, B, c)}
(irl-ntriple) ¬R(a, b) 7! {¬triplea(a, R, b, c)} (irl-subr) R v S 7! {subRole(R, S, c)}
(irl-eq) a = b 7! {eq(a, b, c)} (irl-subrc) R S v T 7! {subRChain(R, S, T, c)}
(irl-neq) a 6= b 7! {¬eq(a, b, c)} (irl-dis) Dis(R, S) 7! {dis(R, S, c)}
(irl-inst3) {a} v B 7! {insta(a, B, c)} (irl-inv) Inv(R, S) 7! {inv(R, S, c)}
(irl-subc) A v B 7! {subClass(A, B, c)} (irl-irr) Irr(R) 7! {irr(R, c)}
(irl-top) >(a) 7! {insta(a, top, c)}
(irl-bot) ?(a) 7! {insta(a, bot, c)}
RL deduction rules Prl
(prl-instd) (¬)instd(x, z, c) (¬)insta(x, z, c).
(prl-tripled) (¬)tripled(x, r, y, c) (¬)tripled(x, r, y, c).
(prl-eq1) eq(x, x, c) nom(x, c).
(prl-eq2) (¬)eq(y, x, c) (¬)eq(x, y, c).
(prl-eq3) (¬)instd(y, z, c) eq(x, y, c), (¬)instd(x, z, c).
(prl-eq4) (¬)tripled(y, u, z, c) eq(x, y, c), (¬)tripled(x, u, z, c).
(prl-eq5) (¬)tripled(z, u, y, c) eq(x, y, c), (¬)tripled(z, u, x, c).
(prl-eq6) (¬)eq(x, z, c) (¬)eq(x, y, c), (¬)eq(y, z, c).
(prl-top) instd(x, top, c) instd(x, z, c).
(prl-subc) instd(x, z, c) subClass(y, z, c), instd(x, y, c).
(prl-not) ¬instd(x, z, c) supNot(y, z, c), instd(x, y, c).
(prl-subcnj) instd(x, z, c) subConj(y1 , y2 , z, c), instd(x, y1 , c), instd(x, y2 , c).
(prl-subex) instd(x, z, c) subEx(v, y, z, c), tripled(x, v, x0 , c), instd(x0 , y, c).
(prl-supex) tripled(x, r, x0 , c) supEx(y, r, x0 , c), instd(x, y, c).
(prl-supforall) instd(y, z 0 , c) supForall(z, r, z 0 , c), instd(x, z, c), tripled(x, r, y, c).
(prl-leqone) eq(x1 , x2 , c) supLeqOne(z, r, z 0 , c), instd(x, z, c), tripled(x, r, x1 , c),
instd(x1 , z 0 , c), tripled(x, r, x2 , c), instd(x2 , z 0 , c).
(prl-subr) tripled(x, w, x0 , c) subRole(v, w, c), tripled(x, v, x0 , c).
(prl-subrc) tripled(x, w, z, c) subRChain(u, v, w, c), tripled(x, u, y, c), tripled(y, v, z, c).
(prl-dis1) ¬tripled(x, v, y, c) dis(u, v, c), tripled(x, u, y, c).
(prl-dis2) ¬tripled(x, u, y, c) dis(u, v, c), tripled(x, v, y, c).
(prl-inv1) tripled(y, v, x, c) inv(u, v, c), tripled(x, u, y, c).
(prl-inv2) tripled(y, u, x, c) inv(u, v, c), tripled(x, v, y, c).
(prl-irr) ¬tripled(x, u, x, c) irr(u, c), nom(x, c).
Table 5. RL input and deduction rules
146