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