Recently, representation of context dependent knowledge in the Semantic 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 metaknowledge 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 translation, 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.
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. [
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 defining 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 represent different independent views of the domain. The global object knowledge is propagated 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.
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 participant. 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 axioms 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 [
We can thus summarize the contributions of our work as follows. After a brief
introduction 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.
Notably, 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
translation for OWL RL based CKR from [
Preliminaries: S ROI Q-RL
This work basically builds on the materialization calculus for CKR on OWL RL
recently proposed in [
C := A | {a} | C1 u C2 | C1 t C2 | 9 R.C1 | 9 R.{a} | 9 R.> D := A | ¬C1 | D1 u D2 | 9 R.{a} | 8 R.D1 | 6 nR.C1 | 6 nR.> 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 interpretation of defeasible inheritance from the upper contexts.
A Contextualized Knowledge Repository (CKR) is a two layered structure. The upper 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 defined 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
2. M ✓ NI of module names. 3. C ✓ NC of context classes, including the class Ctx.
DA ✓
5. A ✓ NR of contextual attributes. 6. For every attribute A 2 A, a set
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 L⌃e 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 [
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 contradicted by an assertion ¬Expensive(concert ), which then overrides the global assertion. 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; however, an assertion ¬Interesting (fbmatch) there would contradict this and should override the instance of the defeasible axiom for fbmatch: that is, the fact ¬Cheap t Interesting (fbmatch) may be violated. 3 The DL language L⌃D 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 Knowledge Repository (CKR) over a meta-vocabulary and an object vocabulary ⌃ is a structure K = hG, {Km}m2 Mi where: – G is a DL knowledge base over L [ L ⌃D , and – every Km is a DL knowledge base over L⌃e , 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 leftconcepts 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 preferences 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 Example 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-Trentinoplatform-for-smart-tourism 4 To keep things simple, we omit modeling sportive events by a separate concept.
Example 4. Our next example shows how we can represent a form of defeasible propagation of information across local contexts using eval expressions. We want to represent 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 G : Kem2012 m : { WorkingNow (alice), WorkingNow (bob), WorkingNow (charlie) } Kem2013 m : ⇢ eval(WorkingNow , {employees2012}) v WorkingBefore,
¬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 [
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,
eval(X, C)I(x) = Se2 CM XI(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.
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 8 x. ↵ (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; intuitively, 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}m2 Mi 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 ✓ d 6= eM for every h↵, ei 2 CAS (x), then I(x) |= ↵ (d).
I(x), if For ↵ 2 L ⌃e 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 model I0CAS = hM0, I0, CAS i of K with M = M0 , it holds I0(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 L ⌃e 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, I0i are CKR models of K such that ICAS = hM, I, CAS i and I0CAS0 = hM0, I0, CAS 0i are justified CAS models of K. Then CtxM = CtxM0 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 INCAS = hM0, I0, CAS 0i the interpretation in which: (i) M0 = {aM | a 2 NI [ NI⌃ }; (ii) M0, I0 and CAS 0 are the restrictions of M, I and CAS to M0 , respectively.
Proposition 2. Let ICAS be a justified CAS -model of K. Then, also the CAS -interpretation INCAS 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 ICAStour = 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 defeasible 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 ICASorg = hM, I, CAS orgi 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 interpretation of Korg we have that {aliceI(x), bobI(x), charlieI(x)} v WorkingBeforeI(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 Propositions 1 and 2 carry over to this setting. 4
CKR translation to general programs
We revise the datalog translation for SROIQ-RL CKR from [
C v 9 A.{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 L⌃e 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 L ⌃D with ↵ of the form of Table 1. It can be seen that for named interpretations, i.e., of the form INCAS , every CKR can be rewritten into an equivalent one in normal form (using new symbols).
A(a)
R(a, b) ¬A(b) ¬R(a, b) a = b a 6= b
A v B 9 R.A v B
{a} v B A v 9 R.{a}
A v ¬B
A v 8 R.B
A u B v C
A v 61R.B R v T
R
S v T
Dis(R, S)
Inv(R, S)
Irr(R)
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 H ead(r) the head a of rule r and with Body+(r) and Body (r) the positive (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 constants occurring in P and the base BP of P as the set of all the ground literals constructible 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.
Using this interpretation for our programs, we say that a literal H 2 BP is a consequence 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 [
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 input translations to knowledge bases (set of axioms) S with their signature ⌃ , with I(S) = S↵ 2 S I(↵ ) [ Ss2 ⌃,I (s) defined I(s) (similarly I(S, c) = S↵ 2 S I(↵, c) [ Ss2 ⌃,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:
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: 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}m2 Mi, 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 2. We define the set of contexts:
} and G⌃ = {↵ 2 G | ↵ 2 L ⌃D }.
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: 4. The CKR program is then defined as:
P C(c) := Ploc [ PD [ Iloc(Kc, c) [ Irl(Kc, c) [ { prec(c, gk).}
P K(K) = P G(G) [ S c2 NG 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 L ⌃e 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 translation 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 NM such that CAS NM(cM) = CAS N(c), for all c 2 N. We can show that the following property holds:
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. [
Lemma 3. For every justified CAS -model ICASNM = hM, I, CASNMi of K, some answer 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 ICASSM = hM, I, CASSMi 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)
framework 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 [
An implementation of the presented translation in a prototype is ongoing. It
basically builds on the DReW DL datalog rewriter [
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 [
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 [
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).
A
Appendix: rules tables
(igl-subctx1) C 2 C 7! { subClass(C, Ctx, gm)} (igl-subctx2) c 2 N 7! { insta(c, Ctx, gm)}
(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)}
(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)} For D(↵ ) 2 S, apply Irl(↵ ) and the corresponding rule in the following: (prop-inst) (¬)instd(x, z, c) (prop-triple) (¬)tripled(x, r, y, c) (prop-subc) instd(x, z, c) (prop-not) ¬instd(x, z, c) (prop-cnj) instd(x, z, c) (prop-subex) instd(x, z, c) (prop-supex) tripled(x, r, x0, c) (prop-forall) instd(y, z0, c) (prop-leqone) eq(x1, x2, c) (prop-subr) tripled(x, w, x0, c) (prop-subrc) tripled(x, w, z, c) (prop-dis1) (prop-dis2) ¬tripled(x, v, y, c) ¬tripled(x, u, y, c) (prop-inv1) tripled(y, v, x, c) (prop-inv2) tripled(y, u, x, c) (prop-irr) ¬tripled(x, u, x, c)
RL input translation Irl(S, c) (irl-nom) (irl-cls) (irl-rol) (irl-inst1) A(a) 7! { insta(a, A, c)} (irl-supex) A v 9 R.{a} 7! { supEx(A, R, a, c)} (irl-inst2) ¬A(a) 7! {¬ insta(a, A, c)} (irl-forall) A v 8 R.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)} (((iiirrrlll---ennqter)qip)le) aa¬ R6==(abb,77!!b){{7!¬e{qe¬(qa(,tabr,,ibc,p)cl})e}a(a, R, b, c)} (((iiirrrlll---ssduuisbb)rr)c) RRDisvS(RSv, S7!T){7 !7!s{{ubsdRuiobslR(eRC(hR,aS,i,Snc,()Rc}),}S, T, c)} (irl-inst3) {a} v B 7! { insta(a, B, c)} (irl-inv) Inv(R, S) 7! { inv(R, S, c)} ((iirrll--tsoupb)c) A>(va) B7! 7!{ {inssutbaC(laa,stso(pA,c,)B}, c)} (irl-irr) Irr(R) 7! { irr(R, c)} (irl-bot) ? (a) 7! { insta(a, bot, c)} RL deduction rules Prl (prl-instd) (¬)instd(x, z, c) (prl-tripled) (¬)tripled(x, r, y, c) (prl-eq1) (prl-eq2) (prl-eq3) (prl-eq4) (prl-eq5) (prl-eq6) eq(x, x, c) (¬)eq(y, x, c) (¬)instd(y, z, c) (¬)tripled(y, u, z, c) (¬)tripled(z, u, y, c) (¬)eq(x, z, c) (prl-subr) (prl-subrc) tripled(x, w, x0, c) tripled(x, w, z, c) (¬)insta(x, z, c). (¬)tripled(x, r, y, c). nom(x, c). (¬)eq(x, y, c). eq(x, y, c), (¬)instd(x, z, c). eq(x, y, c), (¬)tripled(x, u, z, c). eq(x, y, c), (¬)tripled(z, u, x, c). (¬)eq(x, y, c), (¬)eq(y, z, c). subRole(v, w, c), tripled(x, v, x0, c). subRChain(u, v, w, c), tripled(x, u, y, c), tripled(y, v, z, c).