Representation of context dependent knowledge in the Semantic Web is becoming a recognized issue and a number of DL-based formalisms have been proposed in this regard: among them, in our previous works we introduced the Contextualized Knowledge Repository (CKR) framework. In CKR, contexts are organized hierarchically according to a broader-narrower relation and knowledge propagation across contexts is limited among contexts hierarchically related. In several applications, however, this structure is too restrictive, as they demand for a more flexible and scalable framework for representing and reasoning about contextual knowledge. In this work we present an evolution of the original CKR (based on OWL RL), where contexts can be organized in any graph based structure (declared as a metaknowledge base) and knowledge propagation is allowed among any pair of contexts via a new ”evaluate-in-context” operator. In particular, we detail a materialization calculus for reasoning over the revised CKR framework and prove its soundness and completeness. Moreover, we outline the current implementation of the calculus on top of SPRINGLES, an extension of standard RDF triple stores for representing and rule-based inferencing over multiple RDF named graphs.
recognized issue and a number of DL-based formalisms have been proposed in this
regard: among them, in our previous works we introduced the Contextualized Knowledge
Repository (CKR) framework [
ple, the context associated to Italian football during 2010 is covered by the context for European sports in the 21st century. Coverage relation regulates the propagation of knowledge across contexts, which is limited among contexts hierarchically related.
Practical applications, however, show that this structure might be too restrictive and demand for a more flexible and scalable representation of contextual knowledge. For example, it is often necessary to: associate a type (e.g. Event) to a set of contexts and characterize it by a set of axioms; use in a context the interpretation of a complex expression from a possibly unrelated class of contexts. For this reason, in this work we extend and generalize the original CKR framework by the following two aspects: 1. Generalizing contextual structure: hierarchical contextual attributes are replaced with a generic graph structure specified by a DL knowledge base, containing individual names to denote contexts (i.e. contexts IDs), identifiers for contextual attributes values, and binary relations that allow to specify the relations and contextual attributes for each context. This generalization enables also the introduction of context classes, prototypical contexts that represent homogeneous classes of contexts.
that allows to refer to the extension of a concept (or role) in another set of contexts.
sion of concept A in contexts of type C is contained in the extension of A in c1. This subsumption enable to propagate the information of A from contexts in C to c1.
checking and prove its soundness and completeness1. Moreover, we outline its current implementation on top of SPRINGLES, an extension of standard RDF triple stores for representing and rule-based inferencing over multiple RDF named graphs. 2
Preliminaries: S ROI Q-RL
tions2 for the logic SROIQ [
OWL RL [
and right-side concept respectively, and defined by the following grammar: C := A | {a} | C1 u C2 | C1 t C2 | ∃R.C1 | ∃R.{a} | ∃R.>
D := A | ¬C1 | D1 u D2 | ∃R.{a} | ∀R.D1 | 6 nR.C1 | 6 nR.> where n ∈ {0, 1}. Finally, a both-side concept E 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 ≡ E.
concept assertions can be only stated in the form D(a), where D is a right-side concept. 3
Contextualized Knowledge Repositories A CKR is a two layered structure. The upper layer is composed of a knowledge base G, which describes two types of knowledge: (i) the structure and the properties of contexts 1 Complete proofs for soundness and completeness are presented in the Appendix. 2 For ease of reference, the intended presentation of syntax and semantics for SROIQ constructors and axioms is presented in Table 4 in the Appendix. 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 containing (locally valid) facts, that can also refer to what holds in other contexts. To favor knowledge reuse, the knowledge of each context is organized in multiple knowledge modules. The association between contexts and modules is represented in the meta-knowledge via a binary relation, and can be either explicitly asserted or inferred via meta-reasoning. The knowledge in a CKR can be expressed by means of any DL language: in the following we provide the parametric definition to any DL language and successively we instantiate it to SROIQ-RL.
vocabulary, containing the elements that define the contextual structure3. Definition 1 (Meta-vocabulary). A meta-vocabulary is a DL vocabulary Γ composed of a set of atomic concepts NCΓ , a set atomic roles NRΓ and a set of individual constants NIΓ that are mutually disjoint and contain the following sets of symbols
including the class Ctx4.
DA ⊆
6. For every attribute A ∈ A, a set
NIΓ of attribute values of A.
The meta-language of a CKR, denoted by LΓ , is a DL language built starting from the meta-vocabulary Γ with the following syntactic conditions on the application of role restrictions: for every • ∈ {∀ , ∃, 6 n, > n}, (i) if the concept • A.B occurs in a concept expression, then B = {a} with a ∈ DA; (ii) if the concept • mod.B occurs in a concept expression, then B = {m} with m ∈ M.
The context (in)dependent knowledge of a CKR is expressed via a DL language called object-language , based on an object-vocabulary Σ = NCΣ ] NRΣ ] NIΣ . The object-language LΣ is the DL language defined starting from the Σ . The expressions of the object language will be evaluated locally to each context: namely each context can interpret each symbol independently. However, there are cases in which one want to constrain the meaning of a symbol in a context with the meaning of a symbol in some other context. For instance if John likes all Indian restaurants in Trento, then the extension of the concept GoodRestaurant in the context of John preferences, contains the extension of IndianRestaurant in the context of tourism in Trento. To represent such external references, we extend the object language LΣ with the so called eval expressions. Given a concept or role expression X of LΣ , and a context expression C of LΓ , an eval expression is an expression of the form eval(X, C). The DL language LΣe extends LΣ with the set of eval-expressions in LΣ . Intuitively, the expression eval(C, {c}) represents the extension of the concept C in the context c. Generalizing, eval(C, C) with C a context class represent the union of the extensions of C in each context of type C. Similar intuition can be given for eval(R, C). The above example can be formalized by adding the following axiom to the context of John’s preferences: eval(IndianRestaurant, {trento tourism}) v GoodRestaurant. Finally, 3 To support readability we use sans-serif typeface to denote elements of the meta-vocabulary. 4 Intuitively, Ctx will be used to denote the class of all contexts. notice that we do not allow nested eval expressions: every expression occurring inside an eval should be an expression in LΣ .
Γ and an object vocabulary Σ , a Contextualized Knowledge Repository (CKR) over hΓ, Σ i is a structure K = hG, {Km}m∈Mi where: – G is a DL knowledge base over LΓ ∪ LΣ – for every module name m ∈ M, Km is a DL knowledge base over LΣe . Definition 3 (S ROIQ-RL CKR). A CKR is a SROIQ-RL CKR, if G is a knowledge base in SROIQ-RL, and for each m ∈ M, Km is a S ROIQ-RL knowledge base, where eval-expressions only occur in left-concepts and contain left-concepts or roles. Example 1. We introduce an example in the tourism recommendation domain5. In this scenario we use CKR to implement a knowledge base, called Ktour, that is populated with touristic events, locations, organizations and tourists’ preferences and profiles, and that is capable to identify events that are interesting for a tourist (or tourists class) starting from his/her preferences. A simplified version of the structure and the conG
Event m_event m_tourist CulturalEvent
SportsEvent Concert
VolleyMatch
VolleyA1
Competition trento_cuneo trento_latina
A1_2012-13 modena_trento m_sport_ev
Tourist m_sp_tourist m_v_match
SportiveTourist CulturalTourist volley_fan_01 m_tourist01 hasParentEvent m_match1 m_match2
m_match3 Kv_match HWoinmneeTre⊑aTmea⊑mT,eaLmos,eHr o⊑sTtTeaemam,..⊑.Team, Kmatch1 Loser(itas_trentino_volley), ...
Winner(bre_banca_cuneo_volley), Ksport_ev eval(Winner, TopMatch) ⊑ TopTeam
eval(TopTeam, SportsEvent) ⊑ Ksp_tourist PreferredTeam
Winner(casa_modena_volley), Kmatch2 Loser(itas_trentino_volley), ...
Winner(itas_trentino_volley),
Kmatch3 Loser(andreoli_latina_volley), ... texts of Ktour is shown in Figure 1. In this example we focus on sportive events and in particular on volley matches. Intuitively, in the global context G, every sport event and tourist is modelled with a context: in the figure, these are depicted as black diamonds and we show some of the official volley matches and a tourist. Contexts are 5 This example is a simplified version of a real case scenario in which we apply CKR to a tourist event recommendation system in Trentino (see http://www.investintrentino.it/ News/Trentour-Trentino-platform-for-smart-tourism ). grouped by types and organized in hierarchies by means of context classes: in the figure (depicted as boxes) we show a distinct context class hierarchy for event types (e.g. SportiveEvent, VolleyMatch) and for tourists types (e.g. SportiveTourist). The metaknowledge in G associates to contexts and context classes a set of knowledge modules, by axioms of the kind Event v ∃mod.{m event} or {modena trento} v ∃mod.{m match2}: in the figure these associations are represented by dotted lines to the gray empty diamonds depicting module name individuals. Knowledge bases associated to modules are depicted as the corresponding gray boxes in the lower part of Figure 1: for example, in Kv match we have general axioms about the structure of volley matches, while in modules for specific matches as Kmatch1 we store assertions about the actual results of the match. Intuitively, the semantics will enforce a form of inheritance of modules via context class hierarchy. Contextual relations across events and tourists are depicted as bold arrows in the figure: the only relation hasParentEvent connects matches with the competition in which they occour. Note that in some of the knowledge modules, we use eval expressions to define references across contexts. For example, in Ksport ev we can state6 that “Winners of major volley matches are top teams” with: eval(W inner, VolleyMatch u ∃hasParentEvent.VolleyA1Competition) v T opT eam Similarly, in Ksp tourist we say that for each sportive tourist “top teams are preferred teams” with eval(T opT eam, SportsEvent) v P ref erredT eam. 3 Definition 4 (CKR interpretation). A CKR interpretation for hΓ, Σ i, is a structure I = hM, Ii s.t. M is a DL interpretation of Γ ∪ Σ and, for every x ∈ CtxM, I(x) is a DL interpretation over Σ .
pretation for the “upper-layer” (which includes the global knowledge and the metaknowledge) and an interpretation of the object language for each instance of type context (i.e., for all x ∈ CtxM), providing a semantics of the object-vocabulary in x. Definition 5 (CKR Model). A CKR interpretation I is a CKR model of K (in symbols, I |= K) iff the following conditions hold: 1. Global interpretation: (i) NM ⊆ CtxM and, for every C ∈ C, CM ⊆ CtxM; (ii) M |= G. 2. Local interpretations: if hx, yi ∈ modM and y = mM, then I(x) |= Km. 3. Knowledge propagation: for every x ∈ CtxM: (i) for a ∈ NIΣ and any y ∈ CtxM, aI(x) = aI(y) = aM; (ii) for α ∈ G with α ∈ LΣ , I(x) |= α .
eval(X, C)I(x) = XI(e) [ e∈CM
which it is evaluated.
ment: intuitively, the problem is specialized by indicating the context of reference. 6 For space reasons, in Figure 1 and in following examples, we write TopMatch as a shortcut for the corresponding context expression.
Definition 6 (c-entailment). Given a CKR K over hΓ, Σ i with c ∈ N and an axiom α ∈ LΣe , we say that α is c-entailed by K (denoted by K |= c : α ) if, for every CKR model I = hM, Ii of K, we have I(cM) |= α . i and an axiom α , we
Definition 7 (Global entailment). Given a CKR K over hΓ, Σ say that α is (globally) entailed by K (denoted by K |= α ) if: – α ∈ LΣe and, for every c ∈ N and model I = hM, Ii of K, we have I(cM) |= α ; – α ∈ LΓ and, for every model I = hM, Ii of K, we have M |= α .
Example 2. We can now consider again the Ktour CKR of Example 1 and provide a formal interpretation for it. Let I = hM, Ii be the model of Ktour directly induced by its assertions. By the definition of the model, we can now find the knowledge base associated to each context: for example, for the context of the match modena trento, we have that I(modena trentoM) |= Kevent ∪ Ksport ev ∪ Kv match ∪ Kmatch2 and similarly for the other matches. In particular, we have that the local interpretation satisfies the axiom eval(W inner, TopMatch) v T opT eam ∈ Ksport ev. We can now give the formal reading of such axiom: we have that eval(W inner, TopMatch)I(modena trentoM) = Se∈TopMatchM W innerI(e). From the assertions in the ABox of G, this corresponds to Se∈{match 2, match 3} W innerI(e). Now, by assertions on W inner inside Kmatch2 and Kmatch3, we obtain {itas trentino, casa modena} ⊆ T opT eamI(modena trentoM).
We have that I(volley fan 01M) |= Ktourist ∪ Ksp tourist ∪ Ktourist01. Thus, the interpretation satisfies eval(T opT eam, SportsEvent) v P ref erredT eam from Ksp tourist. As in the case above, eval(T opT eam, SportsEvent)I(volley fan 01M) is interpreted as Se∈SportsEventM T opT eamI(e). From the assertions in G, we obtain that this is equal to Se∈{match 1, match 2, match 3} T opT eamI(e). Finally, from the reference axiom above, we obtain {itas trentino, casa modena} ⊆ P ref erredT eamI(volley fan 01M). 3 4
Materialization Calculus Kic In this section we extend the materialization calculus Kinst for instance checking on
structure of a CKR in SROIQ-RL. As we will discuss in the following, this calculus basically formalizes the operation of forward closure we realized in the implementation.
the considered axioms. We say that a CKR K = hG, {Km}m∈Mi is in normal form if: – G contains axioms in LΓ of the form of Table 1 or in the form C v ∃mod.{m},
C v ∃A.{dA} for A, B, C ∈ C, R, S, T ∈ R, a, b ∈ N, m ∈ M, A ∈ A and dA ∈ 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 ∈ NC, a, b ∈ NI, R, S, T ∈ NR and C ∈ C.
A v B ∃R.A v B
R(a, b)
{a} v B A v ∃R.{a} ¬R(a, b) a = b R v T
R ◦ S v T
Dis(R, S)
Inv(R, S)
Irr(R)
We can give a set of rules7 that can be used to transform any SROIQ-RL CKR in
an “equivalent” CKR in normal form. As in [
Lemma 1. For every CKR K = hG, {Km}m∈Mi over hΓ, Σ i, a CKR K0 over extended vocabularies hΓ 0, Σ 0i can be computed in linear time s.t. all axioms in K0 are in normal form and, for all axioms α only using symbols from hΓ, Σ i, K |= α iff K0 |= α .
tu
sentation given in [
predicates. We assume a set V of variables and we call terms the elements of C ∪ V.
for i ∈ {1, . . . , n}. A rule is an expression in the form B1, . . . , Bm → H where H and B1, . . . , Bm are datalog atoms (the head and body of the rule). A fact H is a ground rule with empty body. A program P is a finite set of datalog rules. A ground substitution σ for hC, Pi is a function σ : V →
C. We define as usual substitutions on atoms and ground instances of atoms. A proof tree for P is a structure hN, E, λ i where hN, Ei is a finite directed tree and λ is a labelling function assigning a ground atom to each node, exists a proof tree for P with root node r and with λ (r) = H. where: for each v ∈ N , there exists a rule B1, . . . , Bm → H in P and a ground substitution σ s.t. (i) λ (v) = σ (H) and (ii) v has m child nodes wi in E, with λ (wi) = σ (Bi) for i ∈ {1, . . . , m}. A ground atom H is a consequence of P (denoted P |= H) if there
undefined or a set of datalog facts; Definition 8 (Materialization calculus Kic). The materialization calculus Kic is composed by the input translations Iglob, Iloc, Irl, the deduction rules Ploc, 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 ∈ N), each I(α ) (or I(α, c)) is either – the set of predicates used by each I, P, O is fixed and finite; – given an axiom α and c ∈ N, O(α, c) is either undefined or a single datalog fact; – all constant symbols in input or output translations for α are signature symbols appearing in (or equal to) α . 7 Presented in Table 5 in the Appendix.
(igl-subctx1) C ∈ C 7→ {subClass(C, Ctx, gm)} (igl-subctx2) c ∈ N 7→ {inst(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) subEval(a, c1, b, c), inst(c0, c1, gm), inst(x, a, c0) → inst(x, b, c) (plc-subevalr) (plc-eq) nom(x, c), eq(x, y, c0) → eq(x, y, c) subEvalR(r, c1, t, c), inst(c0, c1, gm), triple(x, r, y, c0) → triple(x, t, y, c) Output translation O(α, c) (o-role) (o-concept) A(a) 7→ {inst(a, A, c)} for global context, input translation Iloc and deduction rules Ploc for local contexts and output rules O are presented in Table 2. Finally, SROIQ-RL input Irl and deduction s∈Σ,I (s) defined I(s, c)). The sets of rules defining input translation Iglob α ∈S I(α ) ∪ S s∈Σ,I (s) defined I(s) (similarly I(S, c) =
lation process” to produce a program that represents the knowledge of the complete input CKR. Let K = hG, {Km}m∈Mi be an input CKR in normal form. Then, let:
P G(G) = Iglob(G) ∪ Prl ∪ Irl(GΓ , gm) ∪ Irl(GΣ , gk) we define its associated knowledge base as: with gm, gk new, GΓ = {α ∈ G | α ∈ LΓ } and GΣ = {α ∈ G | α ∈ LΣ }. We define the set of contexts NG = {
c ∈ C | P G(G) |= inst(c, Ctx, gm)}. For every c ∈ NG, Kc = [
{Km ∈ K | P G(G) |= triple(c, mod, m, gm)}
P C(c) = Ploc ∪ Iloc(Kc, c) ∪ Irl(Kc, c) ∪ Irl(GΣ , c) Finally, the program for K can be encoded as P K(K) = P G(G) ∪ S c∈NG
P C(c).
We say that G entails an axiom α
∈ LΓ (denoted G ` α ) if P G(G) and O(α, gm) gm with gk. We say that K entails an axiom α are defined and P G(G) |= O(α, gm). The same can be stated if α ∈ LΣ e in a context c ∈ N (denoted ∈ LΣ , substituting K ` c : α ) if the elements of P K(K) and O(α, c) are defined and P K(K) |= O(α, c).
calculus for instance checking (with respect to c-entailment) in SROIQ-RL CKRs in
normal form. The result can be verified by extending the proofs in [
Theorem 1 (Soundness). Given K = hG, {Km}m∈Mi a CKR in normal form, α ∈ LΣ an atomic concept or role assertion and c ∈ N, then K ` c : α implies K |= c : α . tu
does not exist c ∈ N ∪ {gm, gk} and a ∈ NIΣ ∪ NIΓ s.t. P K(K) |= inst(a, bot, c). Lemma 3. Given K = hG, {Km}m∈Mi a consistent CKR in normal form, and α ∈ LΓ or α ∈ LΣ with α an atomic concept or role assertion, then G |= α implies G ` α . Theorem 2 (Completeness). Given K = hG, {Km}m∈Mi a consistent CKR in normal form, α ∈ LΣ an atomic concept or role assertion and c ∈ N, then K |= c : α implies tu tu
Concrete Syntax for RDF with Named Graphs The forward reasoning over CKR expressed by the materialization calculus has been implemented in a prototype. Basically, the prototype accepts RDF input data expressing OWL-RL axioms and assertions for global and local knowledge modules: these different pieces of knowledge are represented as distinct named graphs, while contextual primitives (e.g. contexts and the eval operator) have been encoded in a RDF vocabulary. The prototype is based on an extension of the Sesame 2.6 framework: the main component, called CKR core module exposes the CKR primitives and a SPARQL 1.1 endpoint for query and update operations on the contextualized knowledge. The module offers the ability to compute and materialize the inference closure of the input CKR, add and remove knowledge and execute queries over the complete CKR structure.
pute inference over multiple graphs in a RDF store. This component has been realized as a general software layer called SPRINGLES8. Intuitively, the layer provides methods to demand a closure materialization on the RDF store data: rules are encoded as SPARQL queries and it is possible to customize both the input ruleset and the evaluation strategy.
calculus. As an example, we present the rule dealing with atomic concept inclusions: :prl-subc a spr:Rule ; spr:head """ GRAPH ?mx { ?x rdf:type ?z } """ ; spr:body """ GRAPH ?m1 { ?y rdfs:subClassOf ?z }
GRAPH ?m2 { ?x rdf:type ?y } GRAPH sys:dep { ?mx sys:derivedFrom ?m1,?m2 } FILTER NOT EXISTS { GRAPH ?m0 { ?x rdf:type ?z }
GRAPH sys:dep { ?mx sys:derivedFrom ?m0 } } """ .
This code corresponds to the local rule (prl-subc) of Prl, thus has the scope of a single context. When the condition in the body part of the rule is verified in graphs ?m1 and ?m2, the head part is materialized in the inference graph ?mx. In the rule we work at level of knowledge modules (i.e. named graphs): the first three lines directly correspond to the rule in Prl; in the fourth line we require that module ?mx, containing the inferences in the given context, depends on the modules of the assumptions. In other words, we require that both rule preconditions and results belong to the KB associated to the same context9. The filter expression checks that the results have not been derived yet.
The rules are evaluated with a strategy that basically follows the same steps of the translation process defined for the calculus. Intuitively, the plan goes as follows: (i) we compute the closure on the graph for global context G, by a fixpoint on rules corresponding to Prl; (ii) we derive associations between contexts and their modules, by adding dependencies for every assertion of the kind mod(c, m) in the global closure; (iii) we compute the closure the contexts, by applying rules encoded from Prl and Ploc and resolving eval expressions by the metaknowledge information in the global closure. 8 SParql-based Rule Inference over Named Graphs Layer Extending Sesame . 9 Statements ?mx sys:derivedFrom ?my are generated from the closure of the global context. For every context, an additional module for its inferences is created and associated to it via sys:derivedFrom relation.
Ktour, can be found at https://dkm.fbk.eu/index.php/CKR-TourismDemo . 6
Related Works
several DL-based formalisms. One relevant example is the Two-dimensional
description logics of context [
LO
and a complex definition of the contextual structure. Contextual modal operators
introduced by this logic allow to define references to other contexts, similarly to the eval
operator. On the other hand, we note that most of the approaches (including [
presented in [
Conclusions
eralizing the previous formalization in aspects of contextual structure and knowledge propagation. We then proposed a sound and complete materialization calculus for reasoning over the new CKR definition and outlined its implementation based on SPARQL and a concrete syntax in RDF with named graphs.
We remark that the newly proposed version addresses several limitations of CKR
in [
rewritings to Datalog programs [
Appendix: Result Proofs
Lemma 1. Given K = hG, {Km}m∈Mi a CKR in normal form, and α ∈ LΓ or α ∈ LΣ with α an atomic concept or role assertion, then G ` α implies G |= α .
in [
mantic condition C(H), P G(G) |= H implies G |= C(H). We can prove the claim by induction on the possible proof tree of the above atoms H. – (prl-ntriple): then H = inst(a, bot, g) and P G(G) |= negtriple(a, R, b, g), P G(G) |= triple(a, R, b, g). We have that ¬R(a, b) ∈ G and, by the above interpretation of atoms, we obtain that G |= R(a, b). This is an absurd, thus there cannot be an interpretation satisfying G, which justifies the consequence G |= ⊥(a). – (prl-eq1): then H = eq(a, a, g) and, by Irl rules, a ∈ NIΓ ∪ NIΣ . For any model M of G, for any a ∈ NIΓ ∪NIΣ it holds that aM = aM, thus this verifies G |= (a = a). – (prl-eq2): then H = eq(b, a, g) and P G(G) |= eq(a, b, g). By the above interpretation of atoms, G |= (a = b): by symmetricity of equality relation this directly implies that G |= (b = a). – (prl-eq3): then H = inst(b, B, g) and P G(G) |= eq(a, b, g), P G(G) |= inst(a, B, g).
By the above interpretation of atoms, G |= (a = b) and G |= B(a). This directly implies that G |= B(b), thus proving the assertion. – (prl-eq4): then H = triple(a, R, b, g) and P G(G) |= eq(c, a, g), P G(G) |= triple(c, R, b, g). By the above interpretation of atoms, G |= (c = a) and G |= R(c, b). This directly implies that G |= R(a, b). The case for (prl-eq5) can be verified similarly. – (prl-eq6): then H = eq(a, b, g) and P G(G) |= eq(a, c, g), P G(G) |= eq(c, b, g).
By the above interpretation of atoms, G |= (a = c) and G |= (c = b): by transitivity of equality relation this directly implies that G |= (a = b). – (prl-neq): then H = inst(a, bot, g) and P G(G) |= neq(a, b, g), P G(G) |= eq(a, b, g). By induction hypothesis and the above semantic conditions, we obtain G |= (a = b) and G |= (a 6= b). This is an absurd, thus there cannot be an interpretation satisfying G: this justifies the consequence G |= ⊥(a). – (prl-top): then H = inst(a, top, g) and P G(G) |= inst(a, B, g). By induction hypothesis, G |= B(a): for every model M of G, it holds that aM ∈ Δ M = >M, thus it is verified that G |= >(a).
Concept constructors atomic concept complement intersection union existential restriction self restriction universal restriction min. card. restriction max. card. restriction cardinality restriction nominal Role constructors atomic role inverse role role composition Axioms
Syntax A ¬C C u D C t D ∃R.C ∃R.Self ∀R.C >nR.C 6nR.C = nR.C {a} Syntax R R− S◦ Q Syntax
Semantics AI Δ I \ CI CI ∩ DI CI ∪ DI x ∈ Δ I ˛˛˛ ∃y. hx, yi ∈ RIff
˛ ∧ y ∈ CI ˘x ∈ Δ I ˛˛ hx, xi ∈ RI ¯ x ∈ Δ I ˛˛˛ ∀y. hx, yi ∈ RIff
˛ → y ∈ CI x ∈ Δ I ˛˛˛ ]{y| hx, yi ∈ RIff
˛ ∧ y ∈ CI } ≥ n x ∈ Δ I ˛˛˛ ]{y| hx, yi ∈ RIff
˛ ∧ y ∈ CI } ≤ n x ∈ Δ I ˛˛˛ ]{y| hx, yi ∈ RIff
˛ ∧ y ∈ CI } = n ˘aI ¯ Semantics RI Semantics ˘hy, xi ˛˛ hx, yi ∈ RI ¯ ˘hx, zi ˛˛ hx, yi ∈ SI , hy, zi ∈ QI ¯ concept inclusion (GCI) C v D CI ⊆ DI concept definition C ≡ D CI = DI role inclusion (RIA) S v R SI ⊆ RI role disjointness Dis(P, R) P I ∩ RI = ∅ reflexivity assertion Ref(R) {hx, xi | x ∈ Δ I } ⊆ RI irreflexivity assertion Irr(R) RI ∩ {hx, xi | x ∈ Δ I } = ∅ symmetry assertion Sym(R) hx, yi ∈ RI ⇒ hy, xi ∈ RI asymmetry assertion Asym(R) hx, yi ∈ RI ⇒ hy, xi ∈/ RI transitivity assertion Tra(R) {hx, yi, hy, zi} ⊆ RI ⇒ hx, zi ∈ RI concept assertion role assertion negated role assertion equality assertion inequality assertion
C(a) R(a, b) ¬R(a, b) a = b a 6= b aI ∈ CI ˙aI , bI ¸ ∈ RI ˙aI , bI ¸ ∈/ RI aI = bI aI 6= bI With A, B ∈ NC, R, S, T ∈ NR, X, Y ∈ NC fresh concept names, W ∈ NR a fresh role name, mx a fresh module name and Kmx its associated knowledge base, C, D, C concept expressions with C, D, C ∈/ NC. G |= T (a, b).
G |= ⊥(a). every model M of G, it holds that bM = cM, which implies G |= (b = c).
G |= R(a, c) with G |= B(b) and G |= B(c). By definition of the semantics, for – (prl-subr): then H = triple(a, S, b, g), R v S ∈ G and P G(G) |= triple(a, R, b, g).
By the above semantic constraints, G |= R(a, b) which directly implies G |= S(a, b). – (prl-subrc): then H = triple(a, T, b, g), R ◦ S v T ∈ G and P G(G) | = triple(a, R, c, g), P G(G) |= triple(c, S, b, g). By the above semantic constraints, G |= R(a, c) and G |= S(c, b): by definition of the semantics, this implies that – (prl-dis): then H = inst(a, bot, g), Dis(R, S) ∈ G and P G(G) |= triple(a, R, b, g), P G(G) |= triple(a, S, b, g). By the above semantic constraints, G |= R(a, b) and G |= S(a, b): this is an absurd, thus there cannot be an interpretation satisfying G, which justifies the consequence G |= ⊥(a).
S(a, b). The case for (prl-inv2) can be proved similarly. – (prl-inv1): then H = triple(a, S, b, g), Inv(R, S) ∈ G and P G(G) |= triple(b, R, a, g).
By the above semantic constraints, G | =
R(b, a): this directly implies that G |= – (prl-irr): then H = inst(a, bot, g), Irr(R) ∈ G and P G(G) |= triple(a, R, a, g).
By induction hypothesis this would imply that G | thus there cannot be an interpretation satisfying G, which justifies the consequence = R(a, a), which is an absurd: tu Theorem 1 (Soundness). Given K = hG, {Km}m∈Mi a CKR in normal form, α ∈ LΣ an atomic concept or role assertion and c ∈ N, then K ` c : α implies K |= c : α .
By definition, P K(K) = P G(G) ∪ S P C(c) = Ploc ∪ Iloc(Kc, c) ∪ Irl(Kc, c) ∪ Irl(GΣ , c).
M |
For Lemma 1, we can also easily derive that, for every interpretation M such that = G: if c ∈ NG (that is, if P G(G) |= inst(c, Ctx, gm)) then cM ∈ CtxM; if Km ∈ Kc (that is, if P G(G) |= triple(c, mod, m, gm)) then cM, mM ∈ modM.
derived from P K(K) as follows, where c ∈ NG: c∈NG
P C(c) where, for every c ∈ NG, – eq(a, b, c) with a, b ∈ NIΣ , then K |= c : a = b; – neq(a, b, c) with a, b ∈ NIΣ , then K |= c : a 6= b; – inst(a, top, c) with a ∈ NIΣ , then K |= c : >(a); – inst(a, bot, c) with a ∈ NIΣ , then K |= c : ⊥(a); – inst(a, A, c) with a ∈ NIΣ , A ∈ NCΣ , then K |= c : A(a); – triple(a, R, b, c) with a, b ∈ NIΣ , R ∈ NRΣ , then K |= c : R(a, b);
mantic condition C(H), P K(K) |= H implies K |= c : C(H). We show the claim by induction on the possible proof tree of the above atoms H: the cases for the rules in Prl are analogous to what has been shown in the previous lemma, thus we only have to prove the assertion for the rules in Ploc.
every model I = hM, Ii of K, S e∈CM AI(e) ⊆
BI(cM) then AI(c0M)
BI(cM) ⊆ and thus I(cM) |= B(a) which means K |= c : B(a). – (plc-subevalr): then H = triple(a, S, b, c) and P K(K) |= subEvalR(R, C, S, c), P K(K) |= inst(c0, C, B, gm) and P K(K) |= triple(a, R, b, c0). By induction hypothesis and Lemma 1, G |= C(c0), K |= c0 : R(a, b). and K |= c : eval(R, C) v S. means K |= c : (a = b).
Hence, for every model I = hM, Ii of K, Se∈CM RI(e) SI(cM) and thus I(cM) |= S(a, b) which means K |= c : S(a, b). ⊆ SI(cM) then RI(c0M) ⊆ – (plc-eq): then H = eq(a, b, c), P K(K) |= nom(a, c) and P K(K) |= eq(a, b, c0). By induction hypothesis, by rules in Irl we have a ∈ NIΣ and K |= c0 : (a = b). Then, for every model I = hM, Ii of K, we have that aI(c0M) = bI(c0M). By the condition on local interpretation of individuals in the definition of CKR model, we have that aI(cM) = aI(c0M) = bI(c0M) = bI(cM). Thus it holds that I(cM) |= (a = b) which – (plc-subeval): then H = inst(a, B, c) and P K(K) |= subEval(A, C, B, c), P K(K) |= inst(c0, C, B, gm) and P K(K) |
= inst(a, A, c0). By induction hypothesis and Lemma 1, G |= C(c0), K |= c0 : A(a) and K |= c : eval(A, C) v B. Hence, for tu tu sociated program. We define the equivalence relation ≈ P K(K) as the reflexive, symmetric and transitive closure of Lemma 2. Let K = hG, {Km}m∈Mi be a CKR in normal form and P K(K) its ason the Herbrand universe of {ha, bi | P K(K) |= eq(a, b, c), for a, b, c ∈ NIΓ ∪ NIΣ } Given a, b, c, d ∈ NIΓ ∪ NIΣ with a ≈ b, it holds that: (i) if P K(K) |= inst(a, A, c), then P K(K) |= inst(b, A, c); (iv) if P K(K) |= inst(d, A, a), then P K(K) |= inst(d, A, b); (ii) if P K(K) |= triple(a, R, d, c), then P K(K) |= triple(b, R, d, c); (iii) if P K(K) |= triple(d, R, a, c), then P K(K) |= triple(d, R, b, c); (v) if P K(K) |= triple(c, R, d, a), then P K(K) |= triple(c, R, d, b); (i) of the assertion. By rule (prl-eq2) and (prl-eq4), we can derive that if Proof. By rules (prl-eq2) and (prl-eq3), it follows immediately that if P K(K) |= eq(a, b, c) then P K(K) |= inst(a, A, c) iff P K(K) |= inst(b, A, c). This also proves point ing point (ii). Point (iii) can be proved similarly by rules (prl-eq2) and (prl-eq5). eq(a, b, c), then P K(K) |= triple(a, R, d, c) iff P K(K) |= triple(b, R, d, c), provP K(K) |= lows from similar reasoning.
For point (iv), let us assume that P K(K) |= inst(d, A, a) with a 6= c (otherwise the assertion is immediate). Then, by the definition of the program, it must be that P G(G) |= eq(a, b, gm). By rules (prl-eq2)-(prl-eq5), in praticular this implies that P G(G) |= triple(a, mod, m, gm) iff P G(G) |= triple(b, mod, m, gm), meaning that, by definition of the translation, they have analogous local programs P C(a) and P C(b) (in which only the “context argument” in the atoms translated by Irl and Iloc changes). Thus, we obtain that P K(K) |= inst(d, A, b). The proof for point (v) folLemma 3. Given K = hG, {Km}m∈Mi a consistent CKR in normal form, and α ∈ LΓ or α ∈ LΣ with α an atomic concept or role assertion, then G |= α implies G ` α . Proof. We show by contrapositive that: G 6` α implies G 6|= α . Assuming that G 6` α , then we have by definition that P G(G) 6|= O(α, gm) if α ∈ LΓ or P G(G) 6|= O(α, gk) if α ∈ LΣ . Let us assume that α ∈ LΓ (the other case can be proved similarly). Then there exists an Herbrand model H of P G(G) such that H 6|= O(α, gm). We show that from this model for P G(G) we can build a model M for G (meeting the definition of the CKR model for the global interpretation) such that M 6|= α , which allow us to derive that G 6|= α .
Let us consider the equivalence relation ≈ as defined in Lemma 2. We define the equivalence classes [c] = {d | d ≈ c}, that will be used to define the domain of the built interpretation.
Then M = hΔ M, · Mi is defined as follows: – Δ M = {[c] | c ∈ NIΓ ∪ NIΣ }; – For each e ∈ Δ M, we define the projection function ι (e) such that, if e = [c], then ι (e) = b with a fixed b ∈ [c]; – cM = [c], for every c ∈ NIΓ ∪ NIΣ ; – AM = {d ∈ Δ M | H |= inst(ι (d), A, g)}, for every A ∈ NCΓ ∪ NCΣ , with g = gm or g = gk; – RM is the smallest set such that hd, d0i ∈ RM if one of the following conditions hold: – H |= triple(ι (d), R, ι (d0), g) with g = gm or g = gk; – S v R ∈ G and hd, d0i ∈ SM; – S ◦ T v R ∈ G and hd, ei ∈ SM, he, d0i ∈ T M for e ∈ Δ M; – Inv(R, S) ∈ G or Inv(S, R) ∈ G and hd0, di ∈ SM;
[c]. It is easy to see that, given α ∈ LΓ with H 6|= O(α, gm), then M 6|= α . For example, if α = C(a), then H 6|= inst(a, C, gm) which implies by definition that M 6|= C(a).
In order to show that M is a model for G, we have to prove that M satisfies the definition of global model from the definition of CKR model, and in particular that M |= G. We easily prove that NM ⊆ CtxM: by the definition of rule (igl-subctx2), for every c ∈ N we have H |= inst(c, Ctx, gm), which implies cM ∈ CtxM. The condition CM ⊆ CtxM for every C ∈ C can be shown similarly by the rule (iglsubctx1). To prove that M |= G, we proceed by cases and consider the form of all of the axioms β ∈ LΓ or β ∈ LΣ that can appear in G. – Let β = A(a) ∈ G, then H |= inst(a, A, g)10. This directly implies that aM = [a] ∈ AM. – Let β = R(a, b) ∈ G, then H |= triple(a, R, b, g). By definition, we directly have that h[a], [b]i ∈ RM. – Let β = ¬R(a, b) ∈ G, then H |= negtriple(a, R, b, g). Suppose that h[a], [b]i ∈ RM, then H |= triple(ι ([a]), R, ι ([b]), g). By rule (prl-ntriple) and Lemma 2, this would imply that H |= inst(ι ([a]), bot, g) contradicting our assumptions on the consistency of K. Thus h[a], [b]i ∈/ RM as required. 10 In the proof of these cases, for simplicity of notation, we assume g = gm or g = gk. – Let β = (a = b) ∈ G, then H |= eq(a, b, g). By the definition of ≈ , it holds that a ≈ b, thus {a, b} ⊆ [a] and aM = bM = [a]. – Let β = (a 6= b) ∈ G, then H |= neq(a, b, g). Suppose that aM = bM, then H |= eq(ι ([a]), ι ([b]), g). By rule (prl-neq) and Lemma 2, we would obtain that H |= inst(ι ([a]), bot, g). Again, this contradicts our assumptions on the consistency of K. Thus aM 6= bM as required. – Let β = {a} v B ∈ G, then H |= inst(a, B, g). This case can be proved similarly to the case β = A(a). – Let β = A v B ∈ G, then H |= subClass(A, B, g). If d ∈ AM, then by definition H |= inst(ι (d), A, g): by rule (prl-subc) we obtain that H |= inst(ι (d), B, g) and thus d ∈ BM. – Let β = >(a) ∈ G, then H |= inst(a, top, g). As in the case for β = A(a) (in which this case is subsumed), we directly obtain that aM = [a] ∈ >M. – Let β = ⊥(a) ∈ G. Assuming that K in input is consistent, this case can not subsist as we would directly derive that H |= inst(a, bot, g), showing the inconsistency of K. – Let β = A v ¬B ∈ G, then H |= supNot(A, B, g). Suppose that d ∈ AM, then H |= inst(ι (d), A, g). Moreover, suppose that d ∈ BM: this implies that H |= inst(ι (d), B, g). By rule (prl-not) and Lemma 2, we would obtain that H |= inst(ι (d), bot, g). This contradicts our assumptions on the consistency of K, thus d ∈/ BM as required. – Let β = A1 u A2 v B ∈ G, then H |= subConj(A1, A2, B, g). If d ∈ A1M and d ∈ A2M, then by definition H |= inst(ι (d), A1, g) and H |= inst(ι (d), A2, g). By rule (prl-subconj), we directly obtain that H |= inst(ι (d), B, g): thus d ∈ BM as required. – Let β = ∃R.A v B ∈ G, then H |= subEx(R, A, B, g). Let d ∈ (∃R.A)M: by definition of the semantics this means that there exists d0 ∈ AM such that hd, d0i ∈ RM. Thus, H |= inst(ι (d0), A, g) and H |= triple(ι (d), R, ι (d0), g). By rule (prl-subex), we obtain that H |= inst(ι (d), B, g): thus d ∈ BM as required. – Let β = A v ∃R.{a} ∈ G, then H |= supEx(A, R, a, g). Let d ∈ AM, then H |= inst(ι (d), A, g). By rule (prl-subex), this implies that H |= triple(ι (d), R, a, g): this proves d, aM ∈ RM as required. – Let β = A v ∀R.B ∈ G, then H |= supForall(A, R, B, g). Let d ∈ AM, then H |= inst(ι (d), A, g). Supposing that there exists d0 ∈ Δ M such that hd, d0i ∈ RM, we have that H |= triple(ι (d), R, ι (d0), g). By rule (prl-supforall) this implies that H |= inst(ι (d0), B, g), thus proving d0 ∈ BM as required. – Let β = A v6 1R.B ∈ G, then H |= supLeqOne(A, R, B, g). Let d ∈ AM, then H |= inst(ι (d), A, g). Suppose that there exist d1, d2 ∈ Δ M such that hd, d1i ∈ RM and hd, d2i ∈ RM, and {d1, d2} ⊆ BM. Thus H |= {triple(ι (d), R, ι (d1), g), triple(ι (d), R, ι (d2), g), inst(ι (d1), B, g), inst(ι (d2), B, g)}. By (prl-leqone) rule we obtain that H |= eq(ι (d1), ι (d2), g). This implies that ι (d1) ≈ ι (d2) and thus they are interpreted as the same domain element d1 = d2 in M. – The cases for β = R v S, R ◦ S v T and Inv(R, S) follow directly from the interpretation of roles in M. – Let β = Dis(R, S) ∈ G, then H |= dis(R, S, g). Suppose that hd, d0i ∈ RM and hd, d0i ∈ SM. Then H |= triple(ι (d), R, ι (d0)g) and H |= triple(ι (d), S, ι (d0)g). By rule (prl-dis) and Lemma 2, we would obtain that H |= inst(ι (d), bot, g). This contradicts our assumptions on the consistency of K, thus there can not exists a pair hd, d0i ∈ RM ∩ SM as required. – Let β = Irr(R) ∈
G, then H |
= irr(R, g). Suppose that hd, di ∈ RM, then thus hd, di ∈/ RM as required.
H | H |= triple(ι (d), R, ι (d), g). By rule (prl-irr) and Lemma 2, we would obtain that = inst(ι (d), bot, g). This contradicts our assumptions on the consistency of K, tu
Theorem 2 (Completeness). Given K = hG, {Km}m∈Mi a consistent CKR in normal form, α ∈ LΣ an atomic concept or role assertion and c ∈ N, then K |= c : α implies K 6|= c : α . for each e ∈ Δ since we can show – Δ c = {[d] | d ∈ NIΣ }; – aI(c) = [a], for every a ∈ NIΣ ;
construction on the global context to the whole structure of the input CKR.
We prove by contrapositive that K 6` c : α implies K 6|= c : α . If K 6` c : α , then
we have by definition that P K(K) 6|=
O(α, c). Then there exists an Herbrand model = O(α, c). As in the previous lemma, from this model for P K(K) we build a CKR model I = hM, Ii for K such that I(cM) 6|= α , implying that We consider again the equivalence relation ≈ defined in Lemma 2 and the equivalence classes [c] = { d | d ≈
c} as from the above lemma. Then we build I = hM, Ii as follows: the global interpretation M = hΔ
M, · Mi is a structure defined as in Lemma 3;
M, we define again the projection function ι (e) such that, if e = [c], then ι (e) = b with a fixed b ∈ [c]. As in the case of Theorem 1, we can note that, M |
= G then: if c ∈ NG (that is, if P G(G) |= inst(c, Ctx, gm)) cM, mM then cM ∈ CtxM; if Km ∈ Kc (that is, if P G(G) |= triple(c, mod, m, gm)) then ∈ modM. For every c ∈ NG, we build I(c) = hΔ c, · I(c)i as follows: – AI(c) = { d ∈ Δ c | H |
= inst(ι (d), A, c)}, for every A ∈ NCΣ ; – RI(c) is the smallest set such that hd, d0i ∈ RI(c) if one of the following conditions hold: – H |= triple(ι (d), R, ι (d0), c); – S v R ∈ Kc ∪ GΣ and hd, d0i ∈ SI(c); – S ◦ T v R ∈ Kc ∪ G
Σ and hd, ei ∈ SI(c), he, d0i ∈ T I(c) for e ∈ Δ c; – Inv(R, S) ∈ Kc ∪ GΣ or Inv(S, R) ∈ Kc ∪ GΣ and hd0, di ∈ SI(c); required. and that I | As in the above lemma, we can see that, given H 6| = O(α, c), then I(cM) 6|= α as
= K. By Lemma 3 we directly obtain that the conditions on the global of ι (e), for every a ∈ NIΣ it holds that aI(x) = aI(y) = aM = [a]. interpretation M are verified. Given x, y ∈ CtxM, we note also that, by the definition
To complete the proof, we have to show that for every Km s.t. c, mM (that is, every Km ∈ Kc) we have I(c) |= Km and I(c) |= GΣ . As in the case above ∈ modM AI(c0), then by definition H | – Let β = eval(A, C) v B ∈ Kc, then H |= subEval(A, C, B, c). If c0 ∈ CM and d ∈ in Kc ∪ GΣ . The case for the axioms in the general normal form of Table 1 can be proved analogously as in the cases of Lemma 3: thus we have to prove the case of local – Let β = eval(R, C) v T ∈ Kc, then H |= subEvalR(R, C, T, c). If there exists = triple(ι (a), R, ι (b), ι (c0)). By rule (plc-evalr) and by Lemma 2 we obtain c0 ∈ CM, then H |
= inst(ι (c0), C, gm). Moreover, suppose ha, bi ∈ RI(c0), then that H |= triple(ι (a), T, ι (b), c), and thus ha, bi ∈ T I(c).