=Paper=
{{Paper
|id=None
|storemode=property
|title=Materialization Calculus for Contexts in the Semantic Web
|pdfUrl=https://ceur-ws.org/Vol-1014/paper_51.pdf
|volume=Vol-1014
|dblpUrl=https://dblp.org/rec/conf/dlog/BozzatoS13
}}
==Materialization Calculus for Contexts in the Semantic Web==
https://ceur-ws.org/Vol-1014/paper_51.pdf
Materialization Calculus for
Contexts in the Semantic Web
Loris Bozzato and Luciano Serafini
Fondazione Bruno Kessler, Via Sommarive 18, 38123 Trento, Italy
{bozzato,serafini}@fbk.eu
Abstract. 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 meta-
knowledge base) and knowledge propagation is allowed among any pair of con-
texts via a new ”evaluate-in-context” operator. In particular, we detail a mate-
rialization 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.
1 Introduction
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 re-
gard: among them, in our previous works we introduced the Contextualized Knowledge
Repository (CKR) framework [13, 4, 2]. In a CKR, each context is associated with a
set of formulae that hold under the same circumstances, which are specified by a set
of dimensional attributes associated to the context (e.g. time, space, topic, author or
access-permissions). In CKR, as proposed in [13], the values of contextual attributes
were organized hierarchically according to a broader-narrower relation. For instance
the geographical value “Italy” is narrower than “Europe”, the time attribute “2010” is
narrower than “21st century”, and the topic attribute “football” is narrower than “sport”.
This structure induces a hierarchical (coverage) relation between contexts. For exam-
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, prototypi-
cal contexts that represent homogeneous classes of contexts.
2. Generalizing knowledge propagation: we introduce the eval operator, a primitive
that allows to refer to the extension of a concept (or role) in another set of contexts.
For instance the subsumption c1 : eval(A, C) v A can be used to state that the exten-
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 .
Over this generalized version of CKR, we detail a materialization calculus for instance
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: SROIQ-RL
In the following we assume the usual presentation of description logics [1] and defini-
tions2 for the logic SROIQ [6].
OWL RL [12] is basically defined on a restriction of SROIQ syntax: in the fol-
lowing we call such restricted language SROIQ-RL. The language is obtained by lim-
iting the form of General 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 | ∃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.
RBox for SROIQ-RL can contain every role axiom of SROIQ but Ref(R). ABox
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 con-
structors and axioms is presented in Table 4 in the Appendix.
of the CKR (called meta-knowledge), and (ii) the knowledge that is context indepen-
dent, i.e., that holds in every context (called global knowledge). The lower layer, is con-
stituted 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.
The meta-knowledge of a CKR is expressed by a DL language defined on a meta-
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 con-
stants NIΓ 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 ∈ A, a set
including the class Ctx4 . DA ⊆ 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 repre-
sent 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 expres-
sion C of LΓ , an eval expression is an expression of the form eval(X, C). The DL
language LeΣ extends LΣ with the set of eval-expressions in LΣ . Intuitively, the ex-
pression eval(C, {c}) represents the extension of the concept C in the context c. Gen-
eralizing, 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 pref-
erences: 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Σ .
Definition 2 (Contextualized Knowledge Repository, CKR). Given a meta-vocabulary
Γ and an object vocabulary Σ, a Contextualized Knowledge Repository (CKR) over
hΓ, Σi is a structure K = hG, {Km }m∈M i where:
– G is a DL knowledge base over LΓ ∪ LΣ
– for every module name m ∈ M, Km is a DL knowledge base over LeΣ .
Definition 3 (SROIQ-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 SROIQ-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 con-
G Event m_tourist
m_event
m_sport_ev Tourist
m_sp_tourist
CulturalEvent SportsEvent
m_v_match SportiveTourist CulturalTourist
VolleyA1
Concert VolleyMatch volley_fan_01
Competition
trento_cuneo trento_latina A1_2012-13
m_tourist01
modena_trento
hasParentEvent
m_match1 m_match2 m_match3
Kv_match HomeTeam ⊑Team, HostTeam ⊑Team, Kmatch1 Winner(bre_banca_cuneo_volley),
Winner ⊑Team, Loser ⊑Team, ... Loser(itas_trentino_volley), ...
Ksport_ev eval(Winner, TopMatch) ⊑ TopTeam Kmatch2 Winner(casa_modena_volley),
Loser(itas_trentino_volley), ...
eval(TopTeam, SportsEvent) ⊑
Ksp_tourist Kmatch3 Winner(itas_trentino_volley),
PreferredTeam Loser(andreoli_latina_volley), ...
Fig. 1. Example CKR knowledge base Ktour
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 di-
amonds 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 asso-
ciated 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 Σ.
According to the previous definition, a CKR interpretation is composed by an inter-
pretation 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 con-
text (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) |= α.
4. Interpretation of eval expressions: given x ∈ CtxM ,
[
eval(X, C)I(x) = X I(e)
e∈CM
Note that the interpretation of an eval expression is independent from the context in
which it is evaluated.
We adapt to CKR models the definition of the classic reasoning problem of entail-
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
α ∈ LeΣ , 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 ) |= α.
We extend this definition to CKR knowledge bases as follows.
Definition 7 (Global entailment). Given a CKR K over hΓ, Σi and an axiom α, we
say that α is (globally) entailed by K (denoted by K |= α) if:
– α ∈ LeΣ 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 as-
sociated 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 for-
M
mal
S reading of such axiom: we have that eval(W inner, TopMatch)I(modena trento ) =
I(e)
M W inner . From the assertions in the ABox of G, this corresponds to
Se∈TopMatch I(e)
e∈{match 2, match 3} W inner . Now, by assertions on W inner inside Kmatch2 and
M
Kmatch3 , we obtain {itas trentino, casa modena} ⊆ T opT eamI(modena trento ) .
We can do a similar reasoning for the context describing the tourist volley fan 01.
We have that I(volley fan 01M ) |= Ktourist ∪ Ksp tourist ∪ Ktourist01 . Thus, the inter-
pretation satisfies eval(T opT eam, SportsEvent) v P ref erredT eam from Ksp tourist .
M
S in the case above, eval(T
As opT eam, SportsEvent)I(volley fan 01 ) is interpreted as
I(e)
M T opT eam . From the assertions in G, we obtain that this is equal to
Se∈SportsEvent
e∈{match 1, match 2, match 3} T opT eamI(e) . Finally, from the reference axiom above,
M
we obtain {itas trentino, casa modena} ⊆ P ref erredT eamI(volley fan 01 )
. 3
4 Materialization Calculus Kic
In this section we extend the materialization calculus Kinst for instance checking on
SROEL(u, ×) (OWL-EL) proposed by [10] in order to reason over the two layered
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.
To simplify the presentation of the calculus rules, we introduce a normal form for
the considered axioms. We say that a CKR K = hG, {Km }m∈M i 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 LeΣ 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(a) R(a, b) ¬R(a, b) a=b a 6= b
AvB {a} v B A v ¬B AuB vC
∃R.A v B A v ∃R.{a} A v ∀R.B A v 61R.B
RvT R◦S vT Dis(R, S) Inv(R, S) Irr(R)
Table 1. Normal form axioms
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 [10], we assume that rule chain axioms in
input are already decomposed in binary role chains. The correctness of this translation
can be shown by the following lemma.
Lemma 1. For every CKR K = hG, {Km }m∈M i over hΓ, Σi, a CKR K0 over extended
vocabularies hΓ 0 , Σ 0 i 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 |= α. t
u
Let us introduce the basic concepts of the proposed calculus. We follow the same pre-
sentation given in [10], and we will thus express our rules in the language of datalog.
A signature is a tuple hC, Pi, with C a finite set of constants and P a finite set of
predicates. We assume a set V of variables and we call terms the elements of C ∪ V.
An atom over hC, Pi is in the form p(t1 , . . . , tn ) with p ∈ P and every ti ∈ 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,
where: for each v ∈ N , there exists a rule B1 , . . . , Bm → H in P and a ground substi-
tution σ 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
exists a proof tree for P with root node r and with λ(r) = H.
We can now present the definition of our materialization calculus: we instantiate
and adapt the general definition given by [10] in order to meet the structure of CKR.
Definition 8 (Materialization calculus Kic ). The materialization calculus Kic is com-
posed 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
undefined or a set of datalog facts;
– given an axiom α and c ∈ N, O(α, c) is either undefined or a single datalog fact;
– the set of predicates used by each I, P, O is fixed and finite;
– all constant symbols in input or output translations for α are signature symbols ap-
pearing in (or equal to) α.
7
Presented in Table 5 in the Appendix.
Global input rules Iglob (G)
(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) subEvalR(r, c1 , t, c), inst(c0 , c1 , gm), triple(x, r, y, c0 ) → triple(x, t, y, c)
(plc-eq) nom(x, c), eq(x, y, c0 ) → eq(x, y, c)
Output translation O(α, c)
(o-concept) A(a) 7→ {inst(a, A, c)}
(o-role) R(a, b) 7→ {triple(a, R, b, c)}
Table 2. Kic translation and deduction rules
Sknowledge bases (set of axioms) S with
We extend the definition of inputStranslations to
their signature Σ, with I(S) = α∈S I(α) ∪ s∈Σ,I(s) defined I(s) (similarly I(S, c) =
S S
α∈S I(α, c)∪ s∈Σ,I(s) defined I(s, c)). The sets of rules defining input translation Iglob
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
Prl rules are presented in Table 3.
In order to introduce the notion of entailment, we define in the following the “trans-
lation process” to produce a program that represents the knowledge of the complete
input CKR. Let K = hG, {Km }m∈M i be an input CKR in normal form. Then, let:
P G(G) = Iglob (G) ∪ Prl ∪ Irl (GΓ , gm) ∪ Irl (GΣ , gk)
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 ,
we define its associated knowledge base as:
[
Kc = {Km ∈ K | P G(G) |= triple(c, mod, m, gm)}
We define the program for c as:
P C(c) = Ploc ∪ Iloc (Kc , c) ∪ Irl (Kc , c) ∪ Irl (GΣ , c)
S
Finally, the program for K can be encoded as P K(K) = P G(G) ∪ c∈NG P C(c).
We say that G entails an axiom α ∈ LΓ (denoted G ` α) if P G(G) and O(α, gm)
are defined and P G(G) |= O(α, gm). The same can be stated if α ∈ LΣ , substituting
gm with gk. We say that K entails an axiom α ∈ LeΣ in a context c ∈ N (denoted
K ` c : α) if the elements of P K(K) and O(α, c) are defined and P K(K) |= O(α, c).
The presented rules and translation provide a sound and complete materialization
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 [10] to SROIQ-RL
and to the CKR structure. Soundness w.r.t. the global knowledge is established as:
Lemma 2. Given K = hG, {Km }m∈M i a CKR in normal form, and α ∈ LΓ or α ∈ LΣ
with α an atomic concept or role assertion, then G ` α implies G |= α. t
u
RL input translation Irl (S, c)
(irl-nom) a ∈ NI 7→ {nom(a, c)} (irl-not) A v ¬B 7→ {supNot(A, B, c)}
(irl-cls) A ∈ NC 7→ {cls(A, c)} (irl-subcnj) A1 u A2 v B 7→ {subConj(A1 , A2 , B, c)}
(irl-rol) R ∈ NR 7→ {rol(R, c)} (irl-subex) ∃R.A v B 7→ {subEx(R, A, B, c)}
(irl-inst1) A(a) 7→ {inst(a, A, c)} (irl-supex) A v ∃R.{a} 7→ {supEx(A, R, a, c)}
(irl-triple) R(a, b) 7→ {triple(a, R, b, c)} (irl-forall) A v ∀R.B 7→ {supForall(A, R, B, c)}
(irl-ntriple) ¬R(a, b) 7→ {negtriple(a, R, b, c)} (irl-leqone) A v 61R.B 7→ {supLeqOne(A, R, B, c)}
(irl-eq) a = b 7→ {eq(a, b, c)} (irl-subr) R v S 7→ {subRole(R, S, c)}
(irl-neq) a 6= b 7→ {neq(a, b, c)} (irl-subrc) R◦S v T 7→ {subRChain(R, S, T, c)}
(irl-inst2) {a} v B 7→ {inst(a, B, c)} (irl-dis) Dis(R, S) 7→ {dis(R, S, c)}
(irl-subc) A v B 7→ {subClass(A, B, c)} (irl-inv) Inv(R, S) 7→ {inv(R, S, c)}
(irl-top) >(a) 7→ {inst(a, top, c)} (irl-irr) Irr(R) 7→ {irr(R, c)}
(irl-bot) ⊥(a) 7→ {inst(a, bot, c)}
RL deduction rules Prl
(prl-ntriple) negtriple(x, v, y, c), triple(x, v, y, c) → inst(x, bot, c)
(prl-eq1) nom(x, c) → eq(x, x, c)
(prl-eq2) eq(x, y, c) → eq(y, x, c)
(prl-eq3) eq(x, y, c), inst(x, z, c) → inst(y, z, c)
(prl-eq4) eq(x, y, c), triple(x, u, z, c) → triple(y, u, z, c)
(prl-eq5) eq(x, y, c), triple(z, u, x, c) → triple(z, u, y, c)
(prl-eq6) eq(x, y, c), eq(y, z, c) → eq(x, z, c)
(prl-neq) eq(x, y, c), neq(x, y, c) → inst(x, bot, c)
(prl-top) inst(x, z, c) → inst(x, top, c)
(prl-subc) subClass(y, z, c), inst(x, y, c) → inst(x, z, c)
(prl-not) supNot(y, z, c), inst(x, y, c), inst(x, z, c) → inst(x, bot, c)
(prl-subcnj) subConj(y1 , y2 , z, c), inst(x, y1 , c), inst(x, y2 , c) → inst(x, z, c)
(prl-subex) subEx(v, y, z, c), triple(x, v, x0 , c), inst(x0 , y, c) → inst(x, z, c)
(prl-supex) supEx(y, r, x0 , c), inst(x, y, c) → triple(x, r, x0 , c)
(prl-supforall) supForall(z, r, z 0 , c), inst(x, z, c), triple(x, r, y, c) → inst(y, z 0 , c)
(prl-leqone) supLeqOne(z, r, z 0 , c), inst(x, z, c), triple(x, r, x1 , c),
inst(x1 , z 0 , c), triple(x, r, x2 , c), inst(x2 , z 0 , c) → eq(x1 , x2 , c)
(prl-subr) subRole(v, w, c), triple(x, v, x0 , c) → triple(x, w, x0 , c)
(prl-subrc) subRChain(u, v, w, c), triple(x, u, y, c), triple(y, v, z, c) → triple(x, w, z, c)
(prl-dis) dis(u, v, c), triple(x, u, y, c), triple(x, v, y, c) → inst(x, bot, c)
(prl-inv1) inv(u, v, c), triple(x, u, y, c) → triple(y, v, x, c)
(prl-inv2) inv(u, v, c), triple(x, v, y, c) → triple(y, u, x, c)
(prl-irr) irr(u, c), triple(x, u, x, c) → inst(x, bot, c)
Table 3. RL input and deduction rules
Soundness for global entailment is proved by extending the result to local knowledge.
Theorem 1 (Soundness). Given K = hG, {Km }m∈M i a CKR in normal form, α ∈ LΣ
an atomic concept or role assertion and c ∈ N, then K ` c : α implies K |= c : α. u
t
Completeness can be verified in a similar way. We say that a CKR K is consistent if there
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∈M i a consistent CKR in normal form, and α ∈ LΓ
or α ∈ LΣ with α an atomic concept or role assertion, then G |= α implies G ` α. u
t
Theorem 2 (Completeness). Given K = hG, {Km }m∈M i a consistent CKR in normal
form, α ∈ LΣ an atomic concept or role assertion and c ∈ N, then K |= c : α implies
K ` c : α. t
u
5 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 express-
ing OWL-RL axioms and assertions for global and local knowledge modules: these dif-
ferent 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 vocabu-
lary. 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 mod-
ule 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.
The distribution of knowledge in different named graphs asks for a module to com-
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.
In our case, the ruleset basically encodes the rules of the presented materialization
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 infer-
ences 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.
A demo of the prototype, containing RDF data that encodes the example CKR
Ktour , can be found at https://dkm.fbk.eu/index.php/CKR-TourismDemo.
6 Related Works
The interest in representation of contexts in the Semantic Web favored the proposal of
several DL-based formalisms. One relevant example is the Two-dimensional descrip-
tion logics of context [8, 9]. It is based on a multimodal extension of one DL with
another: the composition of an object language LO with a contextual language LC re-
sults in a combined language CL C
LO . This allows a clear separation of the metaknowledge
and a complex definition of the contextual structure. Contextual modal operators intro-
duced 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 [13]) only
consider fixed structures for the representation of metaknowledge, possibly for dealing
with the complexity of the combination of languages [7, 14–16]. A comparison of the
approaches with respect to the needs for context in Semantic Web can be found in [3].
The presented materialization calculus extends the calculus for instance checking
presented in [10] for SROEL(u, ×) to the language of OWL RL: in our extension, we
also referred to the subsequent work [11] presenting a rule-based calculus for classifi-
cation in OWL RL.
7 Conclusions
In this paper we presented a revised and extended version of the CKR framework, gen-
eralizing the previous formalization in aspects of contextual structure and knowledge
propagation. We then proposed a sound and complete materialization calculus for rea-
soning 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 [13]: the global context G extends the metaknowledge component of CKR with
global object knowledge and, most of all, metaknowledge is not limited by a fixed
structure but can be defined as a full DL knowledge base; contextual structure is now
independent from the definition of context dimensions and the coverage relation, while
general context relations can be explicitly asserted across contexts; the eval operator
generalizes the notion of qualified symbols to generic object expressions and contexts
classes; finally, we allow multiple modules to be associated to contexts. On the other
hand we have still to verify how this increase in representation potential affects the
complexity of reasoning in the new representation.
We are currently realizing a different implementation of the calculus based on DL
rewritings to Datalog programs [5]. Moreover we plan to study the complexity proper-
ties of the new version of the CKR with respect to the previous formalization. Finally,
we want to evaluate the different realizations of CKR with respect to reasoning perfor-
mances and ease of modelling over the same set of contextualized data, as in [2].
References
1. Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P. (eds.): The De-
scription Logic Handbook. Cambridge University Press (2003)
2. Bozzato, L., Ghidini, C., Serafini, L.: Comparing contextual and flat representations of
knowledge – a concrete case about football data. In: K-Cap 2013 (2013)
3. Bozzato, L., Homola, M., Serafini, L.: Context on the semantic web: Why and how. In:
ARCOE-12 (2012)
4. 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)
5. Heymans, S., Eiter, T., Xiao, G.: Tractable reasoning with dl-programs over datalog-
rewritable description logics. In: ECAI 2010. Frontiers in Artificial Intelligence and Ap-
plications, vol. 215, pp. 35–40. IOS Press (2010)
6. Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible SROIQ. In: KR 2006. pp.
57–67. AAAI Press (2006)
7. Khriyenko, O., Terziyan, V.: A framework for context sensitive metadata description. IJSMO
1(2), 154–164 (2006)
8. Klarman, S.: Reasoning with Contexts in Description Logics. Ph.D. thesis, Free University
of Amsterdam (2013)
9. Klarman, S., Gutiérrez-Basulto, V.: Two-dimensional description logics of context. In:
DL2011. CEUR-WP, vol. 745, pp. 235–245. CEUR-WS.org (2011)
10. Krötzsch, M.: Efficient inferencing for owl el. In: JELIA 2010. Lecture Notes in Computer
Science, vol. 6341, pp. 234–246. Springer (2010)
11. Krötzsch, M.: The not-so-easy task of computing class subsumptions in OWL RL. In: ISWC
2012. Lecture Notes in Computer Science, vol. 7649, pp. 279–294. Springer (2012)
12. 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/
13. Serafini, L., Homola, M.: Contextualized knowledge repositories for the semantic web. J. of
Web Semantics 12, 64–87 (2012)
14. Straccia, U., Lopes, N., Lukácsy, G., Polleres, A.: A general framework for representing and
reasoning with annotated semantic web data. In: AAAI 2010, Special Track on Artificial
Intelligence and the Web. AAAI Press (July 2010)
15. Tanca, L.: Context-Based Data Tailoring for Mobile Users. In: BTW 2007 Workshops. pp.
282–295 (2007)
16. Udrea, O., Recupero, D., Subrahmanian, V.S.: Annotated RDF. ACM Trans. Comput. Log.
11(2), 1–41 (2010)
A Appendix: Result Proofs
A.1 Soundness
Lemma 1. Given K = hG, {Km }m∈M i a CKR in normal form, and α ∈ LΓ or α ∈ LΣ
with α an atomic concept or role assertion, then G ` α implies G |= α.
Proof. We can basically follow the same proof schema used for proving soundness
in [10], by adapting it to the rules of our calculus. By definition, we have that P G(G) =
Iglob (G) ∪ Prl ∪ Irl (GΓ , gm) ∪ Irl (GΣ , gk). We can assign an interpretation to the
ground atoms derived from P G(G) as follows, where g = gm or g = gk:
– inst(a, A, g) with a ∈ NIΓ ∪ NIΣ , A ∈ NCΓ ∪ NCΣ , then G |= A(a);
– inst(a, top, g) with a ∈ NIΓ ∪ NIΣ , then G |= >(a);
– inst(a, bot, g) with a ∈ NIΓ ∪ NIΣ , then G |= ⊥(a);
– triple(a, R, b, g) with a, b ∈ NIΓ ∪ NIΣ , R ∈ NRΓ ∪ NRΣ , then G |= R(a, b);
– eq(a, b, g) with a, b ∈ NIΓ ∪ NIΣ , then G |= a = b;
– neq(a, b, g) with a, b ∈ NIΓ ∪ NIΣ , then G |= a 6= b;
We claim that, for any ground atom H of the above form with the corresponding se-
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 inter-
pretation 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 interpreta-
tion 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 interpre-
tation 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 Syntax Semantics
atomic concept A AI
complement ¬C ∆I \ C I
intersection C uD C I ∩ DI
I I
union C tD ∪D ˛
C
˛ ∃y. hx, yi ∈ RI
ff
existential restriction ∃R.C x ∈ ∆I ˛˛ I
˘ I ˛
˛ ∧ y ∈ C I¯
self restriction ∃R.Self x ∈ ∆ ˛hx, xi ∈ R I
ff
I ˛ ∀y. hx, yi ∈ R
˛
universal restriction ∀R.C x∈∆ ˛
→ y ∈ CI
˛ ]{y| hx, yi ∈ RI
˛ ff
min. card. restriction >nR.C x ∈ ∆I ˛˛ I
˛ ∧ y ∈ C } ≥ nI ff
]{y| hx, yi ∈ R
x ∈ ∆I ˛˛
˛
max. card. restriction 6nR.C I
˛ ∧ y ∈ C } ≤ nI ff
˛ ]{y| hx, yi ∈ R
cardinality restriction = nR.C x ∈ ∆I ˛˛
∧ y ∈ CI } = n
˘ I¯
nominal {a} a
Role constructors Syntax Semantics
I
atomic role R R
R− hy, xi ˛˛ hx, yi ∈ RI
˘ ˛ ¯
inverse role
hx, zi ˛ hx, yi ∈ S I , hy, zi ∈ QI
˘ ¯
role composition S◦Q
Axioms Syntax Semantics
concept inclusion (GCI) CvD C I ⊆ DI
concept definition C≡D C I = DI
role inclusion (RIA) SvR S I ⊆ 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} ⊆ R ⇒ hx, zi ∈ RI
I
I I
concept assertion C(a) ˙ I∈ C
a
I
¸ I
role assertion R(a, b) ˙aI , bI ¸ ∈ RI
negated role assertion ¬R(a, b) a ,b ∈ /R
equality assertion a=b aI = bI
inequality assertion a 6= b aI 6= bI
Table 4. Syntax and Semantics of SROIQ
C(a) 7→ {X(a), X v C} Sym(P ) 7→ {P v W, Inv(P, W )}
C v D 7→ {C v X, X v D} Trans(P ) 7→ {P ◦ P v P }
A v > 7→ ∅ Asym(P ) 7→ {Dis(P, W ), Inv(P, W )}
⊥ v A 7→ ∅
eval(D, C) v B ∈ Km 7→ {eval(X, Y ) v B ∈ Km ,
A v ¬C 7→ {A v ¬X, C v X} D v X∈ Kmx , C v Y ∈ G,
C u A v B 7→ {C v X, X u A v B} Y v ∃mod.{mx} ∈ G}
A v C u D 7→ {A v C, A v D} eval(R, C) v T ∈ Km 7→ {eval(R, Y ) v T ∈ Km ,
C t D v B 7→ {C v B, D v B} C v Y ∈ G}
∃R.C v A 7→ {C v X, ∃R.X v A} ∃eval(R, C).A v B ∈ Km 7→ {∃W.A v B ∈ Km ,
A v ∃R.C 7→ {A v ∃R.X, C v X} eval(R, C) v W ∈ Km }
A v ∀R.D 7→ {A v ∀R.X, X v D} eval(R, C) ◦ S v T ∈ Km 7→ {eval(R, C) v W ∈ Km ,
A v 60R.D 7→ {A v ∀R.¬D} W ◦ S v T ∈ Km }
A v 61R.D 7→ {A v 61R.X, D v X} Dis(eval(R, C), S) ∈ Km 7→ {eval(R, C) v W ∈ Km ,
Dis(W, S) ∈ Km }
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.
Table 5. Normal form transformation
– (prl-subc): then H = inst(a, B, g), A v B ∈ G and P G(G) |= inst(a, A, g). By
the above semantic conditions, G |= A(a): this directly implies that G |= B(a).
– (prl-not): then H = inst(a, bot, g), A v ¬B ∈ G and P G(G) |= inst(a, A, g),
P G(G) |= inst(a, B, g). By induction hypothesis, G |= A(a) and G |= B(a): this
is an absurd, since the first consequence would imply that G |= (¬B)(a). Thus there
can not be an interpretation satisfying G, which justifies the consequence G |= ⊥(a).
– (prl-subcnj): then H = inst(a, B, g), AuC v B ∈ G and P G(G) |= inst(a, A, g),
P G(G) |= inst(a, C, g). By the above semantic conditions, G |= A(a) and G |=
C(a): this directly implies that G |= (A u C)(a), and thus G |= B(a).
– (prl-subex): then H = inst(a, B, g), ∃R.A v B ∈ G and P G(G) |= triple(a, R, b, g),
P G(G) |= inst(b, A, g). By induction hypothesis, this implies that G |= R(a, b)
and G |= A(b): by definition of the semantics, this proves that G |= (∃R.A)(a)
which implies G |= B(a).
– (prl-supex): then H = triple(a, R, b, g), A v ∃R.{b} ∈ G and P G(G) |=
inst(a, A, g). By induction hypothesis, G |= A(a): this implies that, for every
model M of G, aM ∈ (∃R.{b})M , that is aM , bM ∈ RM . This proves that
G |= R(a, b).
– (prl-supforall): then H = inst(b, B, g), A v ∀R.B ∈ G and P G(G) |= inst(a, A, g),
P G(G) |= triple(a, R, b, g). By induction hypothesis, G |= A(a) and G |=
R(a, b): this implies that, for every model M of G, aM ∈ (∀R.B)M , and thus
bM ∈ B M . This proves that G |= B(b).
– (prl-leqone): then H = eq(b, c, g), A v6 1R.B ∈ G. Moreover, P G(G) |=
inst(a, A, g), P G(G) |= triple(a, R, b, g) with P G(G) |= inst(b, B, g) and
P G(G) |= triple(a, R, c, g) with P G(G) |= inst(c, B, g). By induction hy-
pothesis, G |= A(a) and thus G |= (6 1R.B)(a). Moreover, G |= R(a, b) and
G |= R(a, c) with G |= B(b) and G |= B(c). By definition of the semantics, for
every model M of G, it holds that bM = cM , which implies G |= (b = c).
– (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
G |= T (a, b).
– (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).
– (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 |=
S(a, b). The case for (prl-inv2) can be proved similarly.
– (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 |= R(a, a), which is an absurd:
thus there cannot be an interpretation satisfying G, which justifies the consequence
G |= ⊥(a).
t
u
Theorem 1 (Soundness). Given K = hG, {Km }m∈M i a CKR in normal form, α ∈ LΣ
an atomic concept or role assertion and c ∈ N, then K ` c : α implies K |= c : α.
Proof. To prove the assertion, we extend the construction of the previous Lemma 1 to
the local interpretations for contexts and the definition of the program representing the
whole input CKR. S
By definition, P K(K) = P G(G) ∪ c∈NG P C(c) where, for every c ∈ NG ,
P C(c) = Ploc ∪ Iloc (Kc , c) ∪ Irl (Kc , c) ∪ Irl (GΣ , c).
For Lemma 1, we can also easily derive that, for every interpretation M such that
M |= 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 .
As in previous lemma, we can assign a semantic constraint to the ground atoms
derived from P K(K) as follows, where c ∈ NG :
– inst(a, A, c) with a ∈ NIΣ , A ∈ NCΣ , then K |= c : A(a);
– inst(a, top, c) with a ∈ NIΣ , then K |= c : >(a);
– inst(a, bot, c) with a ∈ NIΣ , then K |= c : ⊥(a);
– triple(a, R, b, c) with a, b ∈ NIΣ , R ∈ NRΣ , then K |= c : R(a, b);
– 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;
We claim that, for any ground atom H of the above form with the corresponding se-
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 .
– (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
M 0M M
every model I = hM, Ii of K, e∈CM AI(e) ⊆ B I(c ) then AI(c ) ⊆ B I(c )
S
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 hy-
pothesis and Lemma 1, G |= C(c0 ), K |= c0 : R(a, b). and K |= c : eval(R, C) v S.
M 0M
Hence, for every model I = hM, Ii of K, e∈CM RI(e) ⊆ S I(c ) then RI(c ) ⊆
S
M
S I(c ) and thus I(cM ) |= S(a, b) which means K |= c : S(a, b).
– (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,
0M 0M
for every model I = hM, Ii of K, we have that aI(c ) = bI(c ) . By the condition
on local interpretation of individuals in the definition of CKR model, we have that
M 0M 0M M
aI(c ) = aI(c ) = bI(c ) = bI(c ) . Thus it holds that I(cM ) |= (a = b) which
means K |= c : (a = b). t
u
A.2 Completeness
Lemma 2. Let K = hG, {Km }m∈M i be a CKR in normal form and P K(K) its as-
sociated program. We define the equivalence relation ≈ on the Herbrand universe of
P K(K) as the reflexive, symmetric and transitive closure 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);
(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);
(iv) if P K(K) |= inst(d, A, a), then P K(K) |= inst(d, A, b);
(v) if P K(K) |= triple(c, R, d, a), then P K(K) |= triple(c, R, d, b);
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
(i) of the assertion. By rule (prl-eq2) and (prl-eq4), we can derive that if P K(K) |=
eq(a, b, c), then P K(K) |= triple(a, R, d, c) iff P K(K) |= triple(b, R, d, c), prov-
ing point (ii). Point (iii) can be proved similarly by rules (prl-eq2) and (prl-eq5).
For point (iv), let us assume that P K(K) |= inst(d, A, a) with a 6= c (other-
wise 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) fol-
lows from similar reasoning. t
u
Lemma 3. Given K = hG, {Km }m∈M i 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 , ·M i 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, d0 i ∈ 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, d0 i ∈ S M ;
– S ◦ T v R ∈ G and hd, ei ∈ S M , he, d0 i ∈ T M for e ∈ ∆M ;
– Inv(R, S) ∈ G or Inv(S, R) ∈ G and hd0 , di ∈ S M ;
Note that by Lemma 2, the definition of M does not depend on the choice of the ι([c]) ∈
[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 (igl-
subctx1). 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
/ RM as required.
consistency of K. Thus h[a], [b]i ∈
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 ∈ B M .
– 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 ∈ B M : 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∈ / B M as required.
– Let β = A1 u A2 v B ∈ G, then H |= subConj(A1 , A2 , B, g). If d ∈ AM 1 and
d ∈ AM 2 , 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 ∈ B M 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, d0 i ∈
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 ∈ B M 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, d0 i ∈ 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 ∈ B M 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, d1 i ∈
RM and hd, d2 i ∈ RM , and {d1 , d2 } ⊆ B M . 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, d0 i ∈ RM and
hd, d0 i ∈ S M . 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, d0 i ∈ RM ∩ S M as required.
– Let β = Irr(R) ∈ G, then H |= irr(R, g). Suppose that hd, di ∈ RM , then
H |= triple(ι(d), R, ι(d), g). By rule (prl-irr) and Lemma 2, we would obtain that
H |= inst(ι(d), bot, g). This contradicts our assumptions on the consistency of K,
/ RM as required.
thus hd, di ∈
t
u
Theorem 2 (Completeness). Given K = hG, {Km }m∈M i a consistent CKR in normal
form, α ∈ LΣ an atomic concept or role assertion and c ∈ N, then K |= c : α implies
K ` c : α.
Proof. As in the case of soundness, we prove the assertion by extending the previous
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
H of P K(K) such that H 6|= 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
K 6|= c : α.
We consider again the equivalence relation ≈ defined in Lemma 2 and the equiva-
lence classes [c] = {d | d ≈ c} as from the above lemma. Then we build I = hM, Ii as
follows: the global interpretation M = h∆M , ·M i is a structure defined as in Lemma 3;
for each e ∈ ∆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,
since we can show M |= G then: 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 . For every c ∈ NG , we build I(c) = h∆c , ·I(c) i as follows:
– ∆c = {[d] | d ∈ NIΣ };
– aI(c) = [a], for every a ∈ NIΣ ;
– AI(c) = {d ∈ ∆c | H |= inst(ι(d), A, c)}, for every A ∈ NCΣ ;
– RI(c) is the smallest set such that hd, d0 i ∈ RI(c) if one of the following conditions
hold:
– H |= triple(ι(d), R, ι(d0 ), c);
– S v R ∈ Kc ∪ GΣ and hd, d0 i ∈ S I(c) ;
– S ◦ T v R ∈ Kc ∪ GΣ and hd, ei ∈ S I(c) , he, d0 i ∈ T I(c) for e ∈ ∆c ;
– Inv(R, S) ∈ Kc ∪ GΣ or Inv(S, R) ∈ Kc ∪ GΣ and hd0 , di ∈ S I(c) ;
As in the above lemma, we can see that, given H 6|= O(α, c), then I(cM ) 6|= α as
required.
To show the assertion, we have to prove that I meets the definition of CKR model
and that I |= K. By Lemma 3 we directly obtain that the conditions on the global
interpretation M are verified. Given x, y ∈ CtxM , we note also that, by the definition
of ι(e), for every a ∈ NIΣ it holds that aI(x) = aI(y) = aM = [a].
To complete the proof, we have to show that for every Km s.t. c, mM ∈ modM
(that is, every Km ∈ Kc ) we have I(c) |= Km and I(c) |= GΣ . As in the case above
we proceed by cases and consider the form of all of the axioms β ∈ LΣ that can appear
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
reference axioms.
– Let β = eval(A, C) v B ∈ Kc , then H |= subEval(A, C, B, c). If c0 ∈ CM and d ∈
0
AI(c ) , then by definition H |= inst(ι(d), A, ι(c0 )) and H |= inst(ι(c0 ), C, gm).
By rule (plc-evalat) we obtain that H |= inst(ι(d), B, c): hence, by definition d ∈
B I(c) .
– Let β = eval(R, C) v T ∈ Kc , then H |= subEvalR(R, C, T, c). If there exists
0
c0 ∈ CM , then H |= inst(ι(c0 ), C, gm). Moreover, suppose ha, bi ∈ RI(c ) , then
H |= triple(ι(a), R, ι(b), ι(c0 )). By rule (plc-evalr) and by Lemma 2 we obtain
that H |= triple(ι(a), T, ι(b), c), and thus ha, bi ∈ T I(c) . t
u