11institutetext: Univ Lyon, MINES Saint-Étienne, CNRS, Laboratoire Hubert
Curien
UMR 5516, F-42023 Saint-Étienne, France
11email<EMAIL_ADDRESS>22institutetext: Université de Lyon, CNRS,
UMR 5516,
Laboratoire Hubert-Curien, Saint-Étienne, France
22email<EMAIL_ADDRESS>
# Integrating Context of Statements within Description Logics

Antoine Zimmermann 11 José M. Giménez-García 22

###### Abstract

We address the problem of providing contextual information about a logical
formula (e.g., provenance, date of validity, or confidence) and representing
it within a logical system. In this case, it is needed to rely on a higher
order or non standard formalism, or some kind of reification mechanism. We
explore the case of reification and formalize the concept of contextualizing
logical statements in the case of Description Logics. Then, we define several
properties of contextualization that are desirable. No previous approaches
satisfy all of the them. Consequently, we define a new way of contextually
annotating statements. It is inspired by NdFluents, which is itself an
extension of the 4dFluents approach for annotating statements with temporal
context. In NdFluents, instances that are involved in a contextual statement
are sliced into contextual parts, such that only parts in the same context
hold relations to one another, with the goal of better preserving inferences.
We generalize this idea by defining contextual parts of relations and classes.
This formal construction better satisfies the properties, although not
entirely. We show that it is a particular case of a general mechanism that
NdFluents also instantiates, and present other variations.

###### Keywords:

Annotations, Contexts, Metadata, Ontologies, Description Logic, Semantic Web,
Reasoning, Reification

##  1 Introduction

The problem of being able to reason not only _with_ logical formulas, but also
_about_ said formulas, is an old one in artificial intelligence. McCarthy [1]
proposed to extend first order logic by reifying context and formulas to
introduce a binary predicate $\mathsf{ist}(\phi,c)$ satisfied if the formula
$\phi$ is true ($\mathsf{ist}$) in the context $c$. However, a complete
axiomatization and calculus for McCarthy’s contextual logic has never been
formalized. Giunchiglia [2] proposed the grouping of “local” formulas in
contexts, and then using other kinds of formulas to characterize how knowledge
from multiple contexts is _compatible_. This idea of locality+compatibility
[3] has led to several non standard formalisms for reasoning with multiple
contexts [4]. Alternatively, the approach of annotated logic programming [5]
considers that a contextual annotation is just a value in an algebraic
structure (e.g., a number or a temporal interval). This idea was later applied
to annotated RDF and RDFS [6, 7].

The representation of statement annotation has sometimes being thought of as a
data model problem without consideration of the logical formalism behind. In
particular, several proposals to extend the RDF data model in various ways for
allowing annotations have been made: named graphs [8], RDF+ [9], RDF* [10],
Yago Model [11]. However, the underlying data structures have not a clear
formal semantics. Therefore, some authors advocate another approach to
representing annotation of knowledge: reify the statement or its context and
describe it within the formalism of the statement. This requires modifying the
statement so as to integrate knowledge of the context or statement. Examples
of such techniques are reification [12], N-Ary Relations [13], Singleton
Property [14]), and NdFluents [15]. _This paper provides an abstraction of the
reification techniques in the context of Description Logics (DLs) in the form
of what we call contextualization functions_. Additionally, we introduce a new
technique for the representation of contextual annotations that satisfies
better some desirable properties.

After introducing our notations for DLs in Sec. 2, we provide formal
definitions that allow us to define verifiable properties of the reification
techniques (Sec. 3). Our new technique, named NdTerms, is presented in Sec. 4,
where we also prove to what extent it satisfies the properties of the previous
section. Sec. 5 discuss some of the problems that may occur when combining
knowledge having different annotations. In Sec. 6, we present how the other
approaches fit in our formalization and why they do not satisfy well the
properties. Finally, we discuss this and future work in Sec. 7.

##  2 Preliminaries

In this section, we introduce the notations and definitions we use in relation
to Description Logics. Note that we use an extended version of DL where all
terms can be used as _concept names_ , _role names_ , and _individual names_
in the same ontology. Using the same name for different types of terms is
known as “punning” in OWL 2 [16, Section 2.4.1]. Moreover, we allow more
constructs than in OWL 2 DL and make no restriction on their use in order to
show that our approach is not limited to a specific DL.

We assume that there is an infinite set of _terms_ $\mathsf{N}$. Every term is
an _individual_. A _role_ is either a term or, given roles $R$ and $S$,
$R\sqcup S$, $R\sqcap S$, $\neg R$, $R^{-}$, $R\circ S$ and $R^{+}$. A
_concept_ is either a term, or, given concepts $C$, $D$, role $R$, individuals
$u_{1},\dots,u_{k}$, and natural number $n$, $\bot$, $\top$, $C\sqcup D$,
$C\sqcap D$, $\exists R.C$, $\forall R.C$, $\leq nR.C$, $\geq nR.C$, $\neg C$
or $\\{u_{1},\dots,u_{k}\\}$. Finally, we also allow concept product $C\times
D$ to define a role.

Interpretations are tuples
$\langle\Delta^{\mathcal{I}},\cdot^{\mathcal{I}_{u}},\cdot^{\mathcal{I}_{r}},\cdot^{\mathcal{I}_{c}}\rangle$,
where $\Delta^{\mathcal{I}}$ is a non-empty set (the domain of interpretation)
and $\cdot^{\mathcal{I}_{u}}$, $\cdot^{\mathcal{I}_{r}}$, and
$\cdot^{\mathcal{I}_{c}}$ are the interpretation functions for individuals,
roles and concepts respectively such that:

  * •

for all $u\in\mathsf{N}$, $u^{\mathcal{I}_{u}}\in\Delta^{\mathcal{I}}$;

  * •

for all $P\in\mathsf{N}$,
$P^{\mathcal{I}_{r}}\subseteq\Delta^{\mathcal{I}}\times\Delta^{\mathcal{I}}$
and interpretation of roles is inductively defined by $(R\sqcup
S)^{\mathcal{I}_{r}}=R^{\mathcal{I}_{r}}\cup S^{\mathcal{I}_{r}}$, $(R\sqcap
S)^{\mathcal{I}_{r}}=R^{\mathcal{I}_{r}}\cap S^{\mathcal{I}_{r}}$, $(\neg
R)^{\mathcal{I}_{r}}=(\Delta^{\mathcal{I}}\times\Delta^{\mathcal{I}})\setminus
R^{\mathcal{I}_{r}}$, $(R^{-})^{\mathcal{I}_{r}}=\\{\langle x,y\rangle|\langle
y,x\rangle\\!\in\\!R^{\mathcal{I}_{r}}\\}$, $(R\circ
S)^{\mathcal{I}_{r}}=\\{\langle x,y\rangle|\exists z.\langle
x,z\rangle\\!\in\\!R^{\mathcal{I}_{r}}\wedge\langle
z,y\rangle\\!\in\\!S^{\mathcal{I}_{r}}\\}$ and $(R^{+})^{\mathcal{I}_{r}}$ is
the reflexive-transitive closure of $R^{\mathcal{I}_{r}}$ (with $R$ and $S$
being arbitrary roles).

  * •

for all $A\in\mathsf{N}$, $A^{\mathcal{I}_{c}}\subseteq\Delta^{\mathcal{I}}$
and interpretation of concepts is defined by
$\bot^{\mathcal{I}_{c}}=\emptyset$,
$\top^{\mathcal{I}_{c}}=\Delta^{\mathcal{I}}$, $(C\sqcup
D)^{\mathcal{I}_{c}}=C^{\mathcal{I}_{c}}\cup D^{\mathcal{I}_{c}}$, $(C\sqcap
D)^{\mathcal{I}_{c}}=C^{\mathcal{I}_{c}}\cap D^{\mathcal{I}_{c}}$, $(\exists
R.C)^{\mathcal{I}_{c}}=\\{x|\exists
y.y\\!\in\\!C^{\mathcal{I}_{c}}\wedge\langle
x,y\rangle\\!\in\\!R^{\mathcal{I}_{r}}\\}$, $(\forall
R.C)^{\mathcal{I}_{c}}=\\{x|\forall y.\langle
x,y\rangle\\!\in\\!R^{\mathcal{I}_{r}}\Rightarrow
y\\!\in\\!C^{\mathcal{I}_{c}}\\}$, $(\leq
nR.C)^{\mathcal{I}_{c}}=\\{x|\sharp\\{y\\!\in\\!C^{\mathcal{I}_{c}}|\langle
x,y\rangle\\!\in\\!R^{\mathcal{I}_{r}}\\}\leq n\\}$, $(\geq
nR.C)^{\mathcal{I}_{c}}=\\{x|\sharp\\{y\\!\in\\!C^{\mathcal{I}_{c}}|\langle
x,y\rangle\\!\in\\!R^{\mathcal{I}_{r}}\\}\geq n\\}$, $(\neg
C)^{\mathcal{I}_{c}}=\Delta^{\mathcal{I}}\setminus C^{\mathcal{I}_{c}}$,
$\\{u_{1},\dots,u_{k}\\}=\\{u_{1}^{\mathcal{I}_{u}},\dots,u_{k}^{\mathcal{I}_{u}}\\}$,
where $C$ and $D$ are arbitrary concepts, $R$ an arbitrary role,
$u_{1},\dots,u_{k}$ are individual names, and $k$ and $n$ two natural numbers.

  * •

Roles defined as a concept product are interpreted as $(C\times
D)^{\mathcal{I}_{r}}=C^{\mathcal{I}_{c}}\times D^{\mathcal{I}_{c}}$ for
arbitrary concepts $C$ and $D$.

In the following, we slightly abuse notations by defining interpretations as
pairs $\langle\Delta^{\mathcal{I}},\cdot^{\mathcal{I}}\rangle$ where
$\cdot^{\mathcal{I}}$ denotes the three functions $\cdot^{\mathcal{I}_{u}}$,
$\cdot^{\mathcal{I}_{c}}$, and $\cdot^{\mathcal{I}_{r}}$. Moreover, when we
write $x^{\mathcal{I}}=y^{\mathcal{I}^{\prime}}$, it means
“$x^{\mathcal{I}_{u}}=y^{\mathcal{I}^{\prime}_{u}}$ and
$x^{\mathcal{I}_{c}}=y^{\mathcal{I}^{\prime}_{c}}$ and
$x^{\mathcal{I}_{r}}=y^{\mathcal{I}^{\prime}_{r}}$”.

_Axioms_ are either general concept inclusions $C\sqsubseteq_{c}D$, sub-role
axioms $R\sqsubseteq_{r}S$, instance assertions $C(a)$, or role assertions
$R(a,b)$, where $C$ and $D$ are concepts, $R$ and $S$ are roles, and $a$ and
$b$ are individual names. An interpretation $\mathcal{I}$ _satisfies_ axiom
$C\sqsubseteq_{c}D$ iff $C^{\mathcal{I}_{c}}\subseteq D^{\mathcal{I}_{c}}$; it
satisfies $R\sqsubseteq_{r}S$ iff $R^{\mathcal{I}_{r}}\subseteq
S^{\mathcal{I}_{r}}$; it satisfies $C(a)$ iff
$a^{\mathcal{I}_{u}}\\!\in\\!C^{\mathcal{I}_{c}}$; and it satisfies $R(a,b)$
iff $\langle
a^{\mathcal{I}_{u}},b^{\mathcal{I}_{u}}\rangle\\!\in\\!R^{\mathcal{I}_{r}}$.
When $\mathcal{I}$ satisfies an axiom $\alpha$, it is denoted by
$\mathcal{I}\models\alpha$. Instance assertions, role assertions and
individual identities constitute the ABox axioms.

An ontology $O$ is composed of a set of terms called the signature of $O$ and
denoted by $\mathsf{Sig}(O)$, and a set of axioms denoted by $\mathsf{Ax}(O)$.
An interpretation $\mathcal{I}$ is a model of an ontology $O$ iff for all
$\alpha\in\mathsf{Ax}(O)$, $\mathcal{I}\models\alpha$. In this case, we write
$\mathcal{I}\models O$. The set of all models of an ontology $O$ is denoted by
$\mathrm{Mod}(O)$. A _semantic consequence_ of an ontology $O$ is a formula
$\alpha$ such that for all $\mathcal{I}\in\mathrm{Mod}(O)$,
$\mathcal{I}\models\alpha$.

In the rest of the paper, we will use teletype font to denote known
individuals, and normal font for unknown individuals and variables (e.g.,
$\mathtt{City}(\mathtt{babylon})$ and $\mathtt{City}(x)$).

##  3 Contextualization of Statements

A contextual annotation can be thought of as a set of ABox axioms that
describe an individual representing the statement (the anchor) that is
annotated. An annotated statement (or ontology) is the combination of a DL
axiom (or DL ontology) with a contextual annotation.

######  Definition 1 (Connected individuals)

Two terms $a$ and $b$ are _connected individuals_ wrt an ABox $A$ iff $a$ and
$b$ are used as individual names in $A$, and either

  * •

$a$ and $b$ are the same term, or

  * •

there exists $R_{1},\cdots,R_{n}$ and $z_{1},\cdots,z_{n-1}$, such that:

    * –

$R_{1}(a,z_{1})$, or $R_{1}(z_{1},a)$

    * –

$R_{i}(z_{i-1},z_{i})$, or $R_{i}(z_{i},z_{i-1})$, $2\leq i\leq n-2$

    * –

$R_{n}(z_{n-1},b)$, or $R_{n}(b,z_{n-1})$

###### Example 1

If we consider the ABox $A=\\{P(a,b),$ $Q(c,b),$ $S(d,e)\\}$, the pairs of
individuals $\\{a,b\\}$, $\\{b,c\\}$, $\\{a,c\\}$, and $\\{d,e\\}$ are
_connected individuals_ , but $\\{a,d\\}$, $\\{b,d\\}$, $\\{c,d\\}$,
$\\{a,e\\}$, $\\{b,e\\}$, and $\\{c,e\\}$ are not.

######  Definition 2 (Contextual annotation)

A _contextual annotation_ $\mathit{Ca}$ is an ABox with signature
$\\{\mathbf{a}\\}\cup\Sigma$ where $\mathbf{a}\not\in\Sigma$ is a
distinguished term (called the _anchor_) and $\Sigma$ is a DL signature such
that $\forall x\in\Sigma$, $\\{a,x\\}$ are _connected individuals_.

###### Example 2

The Abox $\mathit{CA}=\\{\mathtt{validity}(\mathbf{a},\mathtt{t}),$
$\mathtt{Interval}(\mathtt{t})$ $\mathtt{from}(\mathtt{t},\mathtt{609BC}),$
$\mathtt{to}(\mathtt{t},\mathtt{539BC})$,
$\mathtt{prov}(\mathbf{a},\mathtt{w}),$
$\mathtt{name}(\mathtt{w},\mathtt{wikipedia}),$ $\mathtt{Wiki}(\mathtt{w})\\}$
is a _contextual annotation_ , where $\mathbf{a}$ is the anchor and
$\Sigma=\\{\mathtt{t},$ $\mathtt{Interval},$ $\mathtt{w},$
$\mathtt{wikipedia},$ $\mathtt{wiki},$ $\mathtt{609BC},$ $\mathtt{539BC}\\}$.

######  Definition 3 (Annotated statement)

An _annotated statement_ is a pair $\langle\alpha,\mathit{Ca}\rangle$ such
that $\alpha$ is a description logic axiom and $\mathit{Ca}$ is a contextual
annotation.

###### Example 3

The pair $\langle\alpha,\mathit{CA}\rangle$, where
$\alpha=\mathtt{capital}(\mathtt{babylon},$ $\mathtt{babylonianEmpire})$ and
$\mathit{CA}$ is the contextual annotation from Ex. 2, is an _annotated
statement_.

######  Definition 4 (Annotated ontology)

An _annotated ontology_ is a pair $\langle O,\mathit{Ca}\rangle$ such that $O$
is a description logic ontology and $\mathit{Ca}$ is a contextual annotation.

Each reification technique has an implicit construction plan in order to map
an annotated statement to a resulting ontology. A contextualization (Def. 5)
represents the procedure that generates a single DL ontology from a given
annotated statement or ontology. The procedure must not lose information,
especially not the annotation.

######  Definition 5 (Contextualization)

A _contextualization_ is a function $f$ that maps each annotated statement
$\alpha_{\mathit{Ca}}=\langle\alpha,\mathit{Ca}\rangle$ to a description logic
ontology $f(\alpha_{\mathit{Ca}})$ =
$\mathsf{St}(\alpha_{\mathit{Ca}})\cup\mathsf{Cx}(\alpha_{\mathit{Ca}})$ such
that:

  * •

there exists an individual $u$ in the signature of
$\mathsf{St}(\alpha_{\mathit{Ca}})$ and of $\mathsf{Cx}(\alpha_{\mathit{Ca}})$
such that:

    * –

for all $R(\mathbf{a},x)\in\mathit{Ca}$,
$R(u,x)\in\mathsf{Cx}(\alpha_{\mathit{Ca}})$;

    * –

for all $R(x,\mathbf{a})\in\mathit{Ca}$,
$R(x,u)\in\mathsf{Cx}(\alpha_{\mathit{Ca}})$;

    * –

for all $C(\mathbf{a})\in\mathit{Ca}$,
$C(u)\in\mathsf{Cx}(\alpha_{\mathit{Ca}})$;

    * –

for all other $\alpha\in\mathit{Ca}$,
$\alpha\in\mathsf{Cx}(\alpha_{\mathit{Ca}})$.

  * •

there is an injective mapping between the signature of $\alpha$ and the
signature of $\mathsf{St}(\alpha_{C})$.

We extend $f$ to all annotated ontologies $O_{\mathit{Ca}}=\langle
O,\mathit{Ca}\rangle$ by defining $f(O_{\mathit{Ca}})=\bigcup_{\alpha\in
O}f(\langle\alpha,\mathit{Ca}\rangle)$.

###### Example 4

An example contextualization function $f_{ex}$ introduces a fresh term $t$ for
each annotated statement with a role assertion $R(a,b)$, where $R$, $a$, and
$b$ are three therms, creates new axioms $\mathtt{subject}(t,s)$,
$\mathtt{predicate}(t,R)$, $\mathtt{object}(t,o)$, and finally removes the
axiom $R(a,b)$. Notice that this construction requires the punning of term
$R$. This function is analogous to _RDF Reification_. The result of this
contextualization, along with Other possible known approaches, is described in
Sec. 6.

Those are the only structures that we will consider in this paper. The
remaining definitions are desirable properties that a contextualization should
satisfy, especially if one wants it to preserve as much of the original
knowledge as possible.

######  Definition 6 (Soundness)

A contextualization function $f$ is _sound_ wrt a set of annotated ontologies
$\Omega$ iff for each $O_{\mathit{Ca}}=\langle O,\mathit{Ca}\rangle\in\Omega$
such that $O$ and $\mathit{Ca}$ are consistent, then $f(O_{\mathit{Ca}})$ is
consistent.

That is, a contextualization is sound if, when contextualizing a consistent
ontology, the result is also consistent. This property avoids that the
contextualization introduces unnecessary contradictions that would result in
everything being entailed by it. Note that this requirement is not necessary
in the opposite direction, i.e., if $f(O_{\mathit{Ca}})$ is consistent, it is
not required that $O$ and $C$ are consistent.

###### Example 5

The contextualization function $f_{ex}$ from Ex. 4 is sound wrt the set of
ontologies $\Omega$, where $\Omega\cup\\{\mathtt{subject},$
$\mathtt{predicate},$ $\mathtt{predicate}\\}=\emptyset$.

######  Definition 7 (Inconsistency preservation)

Let $f$ be a contextualization function. We say that $f$ preserves
inconsistencies iff for all annotated ontologies $O_{\mathit{Ca}}=\langle
O,\mathit{Ca}\rangle$, if $O$ is inconsistent then $f(O_{\mathit{Ca}})$ is
inconsistent.

Inconsistency preservation means that a self-contradictory ontology in a given
context is contextualized into an inconsistent ontology, such that bringing
additional knowledge from other contexts would result in no more consistency.
If something is inconsistent within a context, then it is not really worth to
consider reasoning with this annotated ontology.

###### Example 6

The contextualization function $f_{ex}$ from Ex. 4 does not preserve
inconsistencies. For instance, $\mathtt{capitalOf}$ can be defined as
irreflexive using the following axiom:
$\exists\mathtt{capitalOf}.\top\sqsubseteq\forall\mathtt{capitalOf^{-}}.\bot$.
Then, the axiom $\mathtt{capitalOf}(\mathtt{babylon},$ $\mathtt{babylon})$
would make the ontology inconsistent. But when applying $f_{ex}$ the result is
consistent.

######  Definition 8 (Entailment preservation)

Let $f$ be a contextualization function. Given two description logic
ontologies $O_{1}$ and $O_{2}$ such that $O_{1}\models O_{2}$, we say that $f$
_preserves the entailment_ between $O_{1}$ and $O_{2}$ iff for all contextual
annotations $\mathit{Ca}$, $f(\langle O_{1},\mathit{Ca}\rangle)\models
f(\langle O_{2},\mathit{Ca}\rangle)$. Given a set
$\mathfrak{K}\subseteq\mathsf{N}^{\mathsf{a}}$ of contextual annotations, if
$f$ preserves all entailments between ontologies in $\mathfrak{K}$, then we
say that $f$ is _entailment preserving_ for $\mathfrak{K}$.

In short, a contextualization is entailment preserving if all the knowledge
that could be inferred from the original ontology can also be inferred, in the
same context, in the contextualized ontology.

###### Example 7

The contextualization function $f_{ex}$ from Ex. 4 preserves entailments for
the TBox of ontologies (because no modifications are made on its axioms), but
it does not preserve entailments on role assertions. For instance, the axioms
$\mathtt{capitalOf}\sqsubseteq\mathtt{cityOf}$,
$\mathtt{capitalOf}(\mathtt{babylon},$ $\mathtt{babylonianEmpire})$ entails
$\mathtt{cityOf}(\mathtt{babylon},$ $\mathtt{babylonianEmpire})$, but this
inference is not preserved after applying $f_{ex}$.

##  4 The NdTerms Approach

This section defines the NdTerms approach that extends the NdFluent proposal
[15]. To this end, we assume that terms are divided into three infinite
disjoint sets $\mathsf{N}^{\mathsf{nc}}$, $\mathsf{N}^{\mathsf{c}}$, and
$\mathsf{N}^{\mathsf{a}}$ called the _non contextual terms_ , the _contextual
terms_ , and the _anchor terms_ respectively. We also assume that there is an
injective function $\mathfrak{A}:\mathfrak{C}\to\mathsf{N}^{\mathsf{a}}$ and
for all $\mathit{Ca}\in\mathfrak{C}$ there is an injective function
$\mathsf{ren}_{\mathit{Ca}}:\mathsf{N}^{\mathsf{nc}}\to\mathsf{N}^{\mathsf{c}}$
and two terms
$\mathtt{isContextualPartOf},\mathtt{isInContext}\in\mathsf{N}^{\mathsf{nc}}$.
For any $\mathit{Ca}$, we extend $\mathsf{ren}_{\mathit{Ca}}$ to axioms by
defining $\mathsf{ren}_{\mathit{Ca}}(\alpha)$ as the axiom built from $\alpha$
by replacing all terms $t\in\mathsf{Sig}(\alpha)$ with
$\mathsf{ren}_{\mathit{Ca}}(t)$.

###  4.1 Contextualization Function in NdTerms

The contextualization needs to combine the ontologies from the statements and
the contextual annotation. However, if we naïvely make the union of the
axioms, they could contradict, and it would not be possible to ensure the
desired properties. For example, an ontology may restrict the size of the
domain of interpretation to be of a fixed cardinality, while the contextual
annotation may rely on more elements outside the local universe of this
context. For this reason we use the concept or relativization: The ontology is
modified in such a way that the interpretation of everything explicitly
described in it is confined to a set, while external terms or constructs may
have elements outside said set. Relativization has been applied in various
logical settings over the past four decades (e.g., [17]) and applied to DLs
and OWL [18], among others.

######  Definition 9 (Relativization)

Let $\mathit{Ca}$ be a contextual annotation. Given an ontology $O$, the
relativization of $O$ in $\mathit{Ca}$ is an ontology
$\mathsf{Rel}_{\mathit{Ca}}(O)$ built from $O$ as follows:

  1. 1.

$\mathsf{Sig}(\mathsf{Rel}_{\mathit{Ca}}(O))=\mathsf{Sig}(O)\cup\top_{\mathit{Ca}}$
where $\top_{\mathit{Ca}}$ is a term not appearing in $\mathsf{Sig}(O)$;

  2. 2.

for all appearances of $\top$ in an axiom of $O$, replace $\top$ with
$\top_{\mathit{Ca}}$;

  3. 3.

for all concepts $\neg C$ appearing in an axiom of $O$, replace it with $\neg
C\sqcap\top_{\mathit{Ca}}$;

  4. 4.

for all roles $\neg R$ appearing in an axiom of $O$, replace it with $\neg
R\sqcap(\top_{\mathit{Ca}}\times\top_{\mathit{Ca}})$;

  5. 5.

for all concepts $\forall R.C$ appearing in an axiom of $O$, replace it with
$\forall R.C\sqcap\top_{\mathit{Ca}}$;

  6. 6.

for all roles $R^{+}$ appearing in an axiom of $O$, replace it with
$R^{+}\sqcap\top_{\mathit{Ca}}\times\top_{\mathit{Ca}}$.

  7. 7.

Additionally, for all terms $t\in\mathsf{Sig}(O)$, the following axioms are in
$\mathsf{Rel}_{\mathit{Ca}}(O)$:

     * •

$t\sqsubseteq\top_{\mathit{Ca}}$,

     * •

$\top_{\mathit{Ca}}(t)$,

     * •

$\exists t.\top\sqsubseteq\top_{\mathit{Ca}}$,

     * •

$\top\sqsubseteq\forall t.\top_{\mathit{Ca}}$.

The relativization of an ontology can be done systematically by relativizing
its concepts and roles, which in turn can be achieved by using Def. 10.

######  Definition 10 (Relativization of concepts and roles)

Given a contextual annotation $\mathit{Ca}$, we define a function
$\mathsf{rel}_{\mathit{Ca}}$ that maps concepts and roles to concepts and
roles according to the rules of Items 2-6. That is, recursively:

  * •

$\mathsf{rel}_{\mathit{Ca}}(t)=t$;

  * •

$\mathsf{rel}_{\mathit{Ca}}(\\{u_{1},\dots
u_{k}\\})=\\{\mathsf{rel}_{\mathit{Ca}}(u_{1}),\dots relf(u_{k})\\}$;

  * •

$\mathsf{rel}_{\mathit{Ca}}(C\sqcup
D)=\mathsf{rel}_{\mathit{Ca}}(C)\sqcup\mathsf{rel}_{\mathit{Ca}}(D)$;

  * •

$\mathsf{rel}_{\mathit{Ca}}(C\sqcap
D)=\mathsf{rel}_{\mathit{Ca}}(C)\sqcap\mathsf{rel}_{\mathit{Ca}}(D)$;

  * •

$\mathsf{rel}_{\mathit{Ca}}(\neg
C)=\neg\mathsf{rel}_{\mathit{Ca}}(C)\sqcap\top_{\mathit{Ca}}$;

  * •

$\mathsf{rel}_{\mathit{Ca}}(C\times
D)=\mathsf{rel}_{\mathit{Ca}}(C)\times\mathsf{rel}_{\mathit{Ca}}(D)$;

  * •

$\mathsf{rel}_{\mathit{Ca}}(R\sqcup
S)=\mathsf{rel}_{\mathit{Ca}}(R)\sqcup\mathsf{rel}_{\mathit{Ca}}(S)$;

  * •

$\mathsf{rel}_{\mathit{Ca}}(R\sqcap
S)=\mathsf{rel}_{\mathit{Ca}}(R)\sqcap\mathsf{rel}_{\mathit{Ca}}(S)$;

  * •

$\mathsf{rel}_{\mathit{Ca}}(R\circ
S)=\mathsf{rel}_{\mathit{Ca}}(R)\circ\mathsf{rel}_{\mathit{Ca}}(S)$;

  * •

$\mathsf{rel}_{\mathit{Ca}}(\neg
R)=\neg\mathsf{rel}_{\mathit{Ca}}(R)\sqcap\top_{\mathit{Ca}}\times\top_{\mathit{Ca}}$;

  * •

$\mathsf{rel}_{\mathit{Ca}}(R^{-})=\mathsf{rel}_{\mathit{Ca}}(R)^{-}$;

  * •

$\mathsf{rel}_{\mathit{Ca}}(R^{+})=\mathsf{rel}_{\mathit{Ca}}(R)^{+}\sqcap\top_{\mathit{Ca}}\times\top_{\mathit{Ca}}$;

  * •

$\mathsf{rel}_{\mathit{Ca}}(\exists
R.C)=\exists\mathsf{rel}_{\mathit{Ca}}(R).\mathsf{rel}_{\mathit{Ca}}(C)$;

  * •

$\mathsf{rel}_{\mathit{Ca}}(\forall
R.C)=\forall\mathsf{rel}_{\mathit{Ca}}(R).\mathsf{rel}_{\mathit{Ca}}(C)\sqcap\top_{\mathit{Ca}}$;

  * •

$\mathsf{rel}_{\mathit{Ca}}(\geq nR.C)=\geq
n~{}\mathsf{rel}_{\mathit{Ca}}(R).\mathsf{rel}_{\mathit{Ca}}(C)$;

  * •

$\mathsf{rel}_{\mathit{Ca}}(\leq nR.C)=\leq
n~{}\mathsf{rel}_{\mathit{Ca}}(R).\mathsf{rel}_{\mathit{Ca}}(C)$.

where $t$ is a term, $C,D$ are concepts, $R,S$ are roles, $u_{1},\dots u_{k}$
are individuals, and $k,n$ are natural numbers.

###### Example 8

The axiom
$\exists\mathtt{capitalOf}.\top\sqsubseteq\forall\mathtt{capitalOf^{-}}.\bot$
from Ex. 6 is relativized into
$\exists\mathtt{capitalOf}.\top_{\mathit{Ca}}\sqsubseteq\forall\mathtt{capitalOf^{-}}.\bot\sqcap\top_{\mathit{Ca}}$.

Then, the contextualization in NdTerms is done by: (1) creating the
replacement of the anchor using the function $\mathfrak{A}$, (2) renaming all
the terms in the statement using the $\mathsf{ren}$ function, (3) linking them
to the original terms by the $\mathtt{isContextualPartOf}$ relation, and (4)
linking the renamed terms to the context using the $\mathtt{isInContext}$
relation.

######  Definition 11 (Contextualization in NdTerms)

Let $\mathit{Ca}\in\mathfrak{C}$ be any contextual annotation. Let
$\alpha_{\mathit{Ca}}=\langle\alpha,\mathit{Ca}\rangle$ be an annotated
statement such that the signatures of $\alpha$ and $\mathit{Ca}$ are in
$\mathsf{N}^{\mathsf{nc}}$. We define the contextualization function
$f_{\mathsf{nd}}$ such that $f_{\mathsf{nd}}(\alpha_{\mathit{Ca}})$ =
$\mathsf{St}(\alpha_{\mathit{Ca}})\cup\mathsf{Cx}(\mathit{Ca})$ and:

  * •

$\mathsf{St}_{\mathit{Ca}}(\alpha)=\\{\mathsf{ren}_{\mathit{Ca}}(\mathsf{Rel}_{\mathit{Ca}}(\alpha))\\}\cup\\{\mathtt{isContextualPartOf}(\mathsf{ren}_{\mathit{Ca}}(t),t)\mid
t\in\mathsf{Sig}(\alpha)\\}\cup\\{\mathtt{isInContext}(\mathsf{ren}_{\mathit{Ca}}(t),\mathfrak{A}(\mathit{Ca}))\mid
t\in\mathsf{Sig}(\alpha)\\}$.

  * •

$\mathsf{Cx}(\mathit{Ca})$ contains exactly the following axioms:

    * –

for all $R(\mathbf{a},x)\in\mathit{Ca}$,
$R(\mathfrak{A}(\mathit{Ca}),x)\in\mathsf{Cx}(\alpha)$;

    * –

for all $R(x,\mathbf{a})\in\mathit{Ca}$,
$R(x,\mathfrak{A}(\mathit{Ca}))\in\mathsf{Cx}(\mathit{Ca})$;

    * –

for all $C(\mathbf{a})\in\mathit{Ca}$,
$C(\mathfrak{A}(\mathit{Ca}))\in\mathsf{Cx}(\mathit{Ca})$;

    * –

for all other axioms $\beta\in\mathit{Ca}$,
$\beta\in\mathsf{Cx}(\mathit{Ca})$.

Similarly to Ex. 4, this construction requires punning, since all terms in the
statement are used as individual names in the role assertion
$\mathtt{isContextualPartOf}(\mathsf{ren}_{\mathit{Ca}}(t),$ $t)$.

###### Example 9

The NdTerms contextualization of our running example within the context
$\mathit{CA}$ of Ex. 2 contains the following axioms, where _term@
$\mathit{Ca}$_ is the result of the renaming function
$\mathsf{ren}_{\mathit{Ca}}($_term_ $)$:

$\mathtt{capitalOf@}(\mathtt{babylon@\mathit{CA}},\mathtt{babylonianEmpire@\mathit{CA}})$

$\mathtt{isContextualPartOf}(\mathtt{babylon@\mathit{CA}},\mathtt{babylon})$

$\mathtt{isContextualPartOf}(\mathtt{babylonianEmpire@\mathit{CA}},\mathtt{babylonianEmpire})$

$\mathtt{isInContext}(\mathtt{babylon},\mathtt{exampleContext})$

$\mathtt{isInContext}(\mathtt{babylonianEmpire},\mathtt{exampleContext})$

$\mathtt{validity}(\mathtt{exampleContext},\mathtt{t})$

$\mathtt{Interval}(\mathtt{t})$

$\mathtt{from}(\mathtt{t},\mathtt{609BC})$

$\mathtt{to}(\mathtt{t},\mathtt{539BC})$

$\mathtt{prov}(\mathtt{exampleContext,\mathtt{w}}$

$\mathtt{name}(\mathtt{w},\mathtt{wikipedia})$

$\mathtt{Wiki}(\mathtt{w})$

###  4.2 Soundness of NdTerms

In this section, we fix a contextual annotation $\mathit{Ka}$ that has its
signature in $\mathsf{N}^{\mathsf{nc}}$, since the following theorems and
proofs require such a constraint.

The contextualization of NdTerms is sound, but only wrt annotated ontologies
that satisfy certain conditions. In order to present the conditions, we need
to introduce the following definition, that is also used in several proofs of
this paper.

######  Definition 12 (Domain extensibility)

Let $O$ be an ontology. A model
$\mathcal{I}=\langle\Delta^{\mathcal{I}},\cdot^{\mathcal{I}}\rangle$ of $O$ is
_domain extensible_ for $O$ iff for all sets $\Delta^{+}$,
$\mathcal{I}^{\prime}=\langle\Delta^{\mathcal{I}}\cup\Delta^{+},\cdot^{\mathcal{I}}\rangle$
is also a model of $O$. An ontology is said to be _model extensible_ iff it
has a model that is domain extensible.

Note that, even if the domain of interpretation of an ontology is infinite,
that does not necessarily mean that its models are domain extensible. This
notion is closely related to the notion of _expansion_ in [18] since if
$\mathcal{I}$ is domain extensible, then one can build infinitely many
expansions of it.

######  Theorem 4.1 (Soundness of NdTerms)

If the contextual annotation $\mathit{Ka}$ is model extensible, then the
contextualization function $f_{\mathsf{nd}}$ is sound wrt annotated ontologies
$O_{\mathit{Ka}}=\langle O,\mathit{Ka}\rangle$,
$\mathsf{Sig}(O)\subseteq\mathsf{N}^{\mathsf{nc}}$, and
$\mathsf{Sig}(O)\cap\mathsf{Sig}(\mathit{Ka})=\emptyset$.

The proof of this theorem requires a few intermediary steps. Theorem 4.2
ensures that, given the right condition, a model of the union of two
ontologies can be made from two models of the original ontologies.

######  Theorem 4.2 (Model extensibility theorem)

Let $O$ and $O^{+}$ be two ontologies such that there exist two models
$\mathcal{I}=\langle\Delta^{\mathcal{I}},\cdot^{\mathcal{I}}\rangle$ and
$\mathcal{I}^{+}\langle\Delta^{\mathcal{I}^{+}},\cdot^{\mathcal{I}^{+}}\rangle$
that are domain extensible for $O$ and $O^{+}$ respectively. If
$\mathsf{Sig}(O)\cap\mathsf{Sig}(O^{+})=\emptyset$ then $\mathcal{I}$ and
$\mathcal{I}^{+}$ can be both extended into a unique model
$\mathcal{I}^{\prime}$ of $O\cup O^{+}$ such that
$\Delta^{\mathcal{I}^{\prime}}=\Delta^{\mathcal{I}}\cup\Delta^{\mathcal{I}^{+}}$
and for all $t\in\mathsf{Sig}(O)$, $t^{\mathcal{I}^{\prime}}=t^{\mathcal{I}}$,
and for all $t\in\mathsf{Sig}(O^{+})$,
$t^{\mathcal{I}^{\prime}}=t^{\mathcal{I}^{+}}$.111Remember from preliminaries
that $t^{\mathcal{I}^{\prime}}=t^{\mathcal{I}}$ means
“$t^{\mathcal{I}^{\prime}_{u}}=t^{\mathcal{I}_{u}}$ and
$t^{\mathcal{I}^{\prime}_{c}}=t^{\mathcal{I}_{c}}$ and
$t^{\mathcal{I}^{\prime}_{r}}=t^{\mathcal{I}_{r}}$”.

######  Proof (Theorem 4.2)

Since $O^{+}$ is consistent, there exists a model $\mathcal{I}^{+}$ of $O^{+}$
and w.l.o.g., we assume that
$\Delta^{\mathcal{I}}\cap\Delta^{\mathcal{I}^{+}}=\emptyset$. We define a new
interpretation $\mathcal{I}^{\prime}$ where
$\Delta^{\mathcal{I}^{\prime}}=\Delta^{\mathcal{I}}\cup\Delta^{+}$; for all
$t\in\mathsf{Sig}(O)$, $t^{\mathcal{I}^{\prime}}=t^{\mathcal{I}}$; and for all
$t\in\mathsf{Sig}(O^{+})$, $t^{\mathcal{I}^{\prime}}=t^{\mathcal{I}^{+}}$. By
definition of domain extensibility, $\mathcal{I}^{\prime}\models O$ and
$\mathcal{I}^{\prime}\models O^{+}$. ∎

From this theorem it follows that NdTerms is sound if both the original
ontology and the contextual annotation are model extensible. However, this is
not a strong restriction, because the relativization of any consistent
ontology is model extensible.

######  Theorem 4.3 (Model extensibility of relativized ontologies)

For any annotated ontology $O_{\mathit{Ka}}=\langle O,\mathit{Ka}\rangle$
where $O$ is consistent, if $\mathsf{Sig}(O)\subseteq\mathsf{N}^{\mathsf{nc}}$
then $\mathsf{Rel}_{\mathit{Ca}}(O)$ is model extensible. and all its models
are domain extensible.

######  Proof (Theorem 4.3)

Since $O$ is consistent, there exists a model
$\mathcal{I}_{o}=\langle\Delta^{\mathcal{I}_{o}},\cdot^{\mathcal{I}_{o}}\rangle$.
We define an interpretation
$\mathcal{I}_{\mathsf{rel}}=\langle\Delta^{\mathcal{I}_{o}},\cdot^{\mathcal{I}_{\mathsf{rel}}}\rangle$
of $\mathsf{Rel}_{\mathit{Ka}}(O)$ where for all $t\in\mathsf{Sig}(O)$,
$t^{\mathcal{I}_{\mathsf{rel}}}=t^{\mathcal{I}_{o}}$ and
$\top_{\mathit{Ka}}^{\mathcal{I}_{\mathsf{rel}}}=\Delta^{\mathcal{I}_{o}}$.

First, we show that $\mathcal{I}_{\mathsf{rel}}$ is a model of
$\mathsf{Rel}_{\mathit{Ka}}(O)$. Indeed, it clearly satisfies all extra axioms
from Item 7 in Def. 9. Second, since
$\top_{\mathit{Ka}}^{\mathcal{I}_{\mathsf{rel}}}=\top^{\mathcal{I}_{\mathsf{rel}}}$,
replacing $\top$ with $\top_{\mathit{Ka}}$ or adding a conjunction with
$\top_{\mathit{Ka}}$ does not change the meaning of the formulas between
$\mathcal{I}_{o}$ and $\mathcal{I}_{\mathsf{rel}}$.

Second, we need to show that any extension of $\mathcal{I}_{\mathsf{rel}}$ is
still a model for $\mathsf{Rel}_{\mathit{Ka}}(O)$, that is,
$\mathcal{I}^{\prime}=\langle\Delta^{\mathcal{I}_{o}}\cup\Delta^{\mathcal{I}^{+}},\cdot^{\mathcal{I}_{\mathsf{rel}}}\rangle\models\mathsf{Rel}_{\mathit{Ka}}(O)$
for any set $\Delta^{\mathcal{I}^{+}}$ such that
$\Delta^{o}\cap\Delta^{\mathcal{I}^{+}}=\emptyset$. Since the interpretations
of the terms are the same in $\mathcal{I}_{\mathsf{rel}}$ and
$\mathcal{I}^{\prime}$, it follows that $\mathcal{I}^{\prime}$ satisfies the
extra axioms in Item 7. We now need to prove that all other axioms of
$\mathsf{Rel}_{\mathit{Ka}}(O)$ are satisfied, which we can do with a proof by
induction taking advantage of the recursive definition of
$\mathsf{rel}_{\mathit{Ka}}$. However, we need to prove an auxiliary lemma.

###### Lemma 1

For all concepts or roles $X$,
$X^{\mathcal{I}_{o}}=\mathsf{rel}_{\mathit{Ka}}(X)^{\mathcal{I}^{\prime}}$.

This lemma can be proved by structural induction on the concepts and roles.
Because of space restriction, we do not provide a complete proof but remark
that every time a construct may lead to a different interpretation due to
increasing the domain of interpretation (e.g., by using the concept $\top$ or
a negation), the function $\mathsf{rel}_{\mathit{Ka}}$ adds a conjunction with
$\top_{\mathit{Ka}}$, so that the interpretations of the relativized concepts
and roles stay confined in the original domain of interpretation.

From this lemma, it follows that if $\mathcal{I}_{o}\models\alpha$ then
$\mathcal{I}^{\prime}\models\mathsf{Rel}_{\mathit{Ka}}(\alpha)$, where
$\alpha$ is any axiom with $\mathsf{Sig}(\alpha)\subseteq\mathsf{Sig}(O)$.
Consequently, $\mathcal{I}^{\prime}\models\mathsf{Rel}_{\mathit{Ka}}(O)$.

In order to prove that all models of $\mathsf{Rel}_{\mathit{Ka}}(O)$ are
domain extensible, we consider an arbitrary model $\mathcal{I}$ of said
ontology and apply the same construction that lead to $\mathcal{I}^{\prime}$
and use the same arguments to show that it is still a model of
$\mathsf{Rel}_{\mathit{Ka}}(O)$. ∎

With Theorem 4.3 proven, we can now proceed to prove the main Theorem 4.1.

######  Proof (Theorem 4.1)

Let us assume that $\mathit{Ka}$ is model extensible. Let $O$ be a consistent
ontology such that $\mathsf{Sig}(O)\cap\mathsf{Sig}(\mathit{Ka})=\emptyset$
and $\mathsf{Sig}(O)\subseteq\mathsf{N}^{\mathsf{nc}}$.

Since $O$ and $\mathit{Ka}$ are consistent, there exist two models
$\mathcal{I}_{o}=\langle\Delta^{\mathcal{I}_{o}},\cdot^{\mathcal{I}_{o}}\rangle$
and $\langle\Delta^{\mathcal{I}_{c}},\cdot^{\mathcal{I}_{c}}\rangle$ of $O$
and $C$ respectively. W.l.o.g., we can assume that
$\Delta^{\mathcal{I}_{o}}\cap\Delta^{\mathcal{I}_{c}}=\emptyset$.

First, from the proof of Theorem 4.3, we know that from a model of $O$, we can
define a model $\mathcal{I}_{\mathsf{Rel}}$ of $\mathsf{Rel}_{\mathit{Ka}}(O)$
having the same domain as $\mathcal{I}_{o}$. Then,
$\mathsf{ren}_{\mathit{Ka}}(\mathsf{Rel}_{\mathit{Ka}}(O))$ is just a renaming
of the terms in $\mathsf{Rel}_{\mathit{Ka}}(O)$, so a new interpretation that
maps the renamed terms to the original interpretation of the original terms
satisfies the renamed ontology.222Since “truth is invariant under change of
notation” [19, Section 2, p.7].

Due to Theorem 4.3, $\mathcal{I}_{\mathsf{Rel}}$ can be extended to include
any additional elements in its domain while remaining a model of
$\mathsf{ren}_{\mathit{Ka}}(\mathsf{Rel}_{\mathit{Ka}}(O))$.

Similarly, $\mathsf{Cx}(\mathit{Ka})$ is like $\mathit{Ka}$ with a renamed
anchor so an interpretation $\mathcal{I}_{\mathfrak{A}}$ that interprets
$\mathfrak{A}(\mathit{Ka})$ as $\mathbf{a}^{\mathcal{I}_{c}}$ and coincides
with $\mathcal{I}_{c}$ on all other terms must be a model of
$\mathsf{Cx}_{\mathit{Ka}}$. Moreover, we assumed that $\mathit{Ka}$ is model
extensible so that $\mathcal{I}_{\mathfrak{A}}$ can be extended to include any
additional elements.

We thus define an interpretation
$\mathcal{I}^{\prime}=\langle\Delta^{\mathcal{I}_{o}}\cup\Delta^{\mathcal{I}_{c}},\cdot^{\mathcal{I}^{\prime}}\rangle$
that extends both $\mathcal{I}_{\mathsf{Rel}}$ and
$\mathcal{I}_{\mathfrak{A}}$ such that:

  * •

for all $t\in\mathsf{Sig}(\mathit{Ka})$,
$t^{\mathcal{I}^{\prime}}=t^{\mathcal{I}_{c}}$;

  * •

for all $t\in\mathsf{Sig}(O)$,
$\mathsf{ren}_{\mathit{Ka}}(t)^{\mathcal{I}^{\prime}}=t^{\mathcal{I}_{o}}$,
and $t^{\mathcal{I}^{\prime}}$ is an arbitrary part of
$\Delta^{\mathcal{I}_{o}}\cup\Delta^{\mathcal{I}_{c}}$;

  * •

$\mathfrak{A}(\mathit{Ka})^{\mathcal{I}^{\prime}}=\mathbf{a}^{\mathcal{I}_{c}}$;

  * •

$\mathtt{isContextualPartOf}^{\mathcal{I}^{\prime}_{r}}=\\{\langle\mathsf{ren}_{\mathit{Ka}}(t)^{\mathcal{I}^{\prime}_{u}},t^{\mathcal{I}^{\prime}_{u}}\rangle\mid
t\in\mathsf{Sig}(O)\\}$;

  * •

$\mathtt{isInContext}^{\mathcal{I}^{\prime}_{r}}=\\{\langle\mathsf{ren}_{\mathit{Ka}}(t)^{\mathcal{I}^{\prime}_{u}},\mathfrak{A}(\mathit{Ka})^{\mathcal{I}^{\prime}_{u}}\rangle\mid
t\in\mathsf{Sig}(O)\\}$.

Let us prove that this interpretation is a model of
$f_{\mathsf{nd}}(O_{\mathit{Ka}})$. Due to the domain extensibility of
$\mathcal{I}_{\mathsf{Rel}}$ and $\mathcal{I}_{\mathfrak{A}}$,
$\mathcal{I}^{\prime}$ remains a model of
$\mathsf{ren}_{\mathit{Ka}}(\mathsf{Rel}_{\mathit{Ka}}(O))$ and of
$\mathsf{Cx}(\mathit{Ka})$

Additionally, the axioms
$\mathtt{isContextualPartOf}(\mathsf{ren}_{\mathit{Ka}}(t),t)$ and
$\mathtt{isInContext}(\mathsf{ren}_{\mathit{Ka}}(t),\mathfrak{A}(\mathit{Ka}))$
are satisfied for all $t\in\mathsf{Sig}(\alpha)$ by definition of
$\mathtt{isContextualPartOf}^{\mathcal{I}^{\prime}_{r}}$ and
$\mathtt{isInContext}^{\mathcal{I}^{\prime}_{r}}$. ∎

###  4.3 Inconsistency Preservation

In this section we prove that NdTerms preserves inconsistencies. As in Sec.
4.2, we fix a contextual annotation $\mathit{Ka}$ that has its signature in
$\mathsf{N}^{\mathsf{nc}}$.

######  Theorem 4.4 (Inconsistency preservation of NdTerms)

The contextualization function $f_{\mathsf{nd}}$ preserves inconsistencies.

######  Proof (Theorem 4.4)

We prove the theorem by contraposition, that is, if $f(O_{\mathit{Ka}})$ is
consistent, then $O$ is consistent.

Let $O_{\mathit{Ka}}=\langle O,\mathit{Ka}\rangle$ be an annotated ontology.
Let us assume that $f(O_{\mathit{Ka}})$ is consistent. There exists a model
$\mathcal{I}=\langle\Delta^{\mathcal{I}},\cdot^{\mathcal{I}}\rangle$ that
satisfies $\mathsf{ren}_{\mathit{Ka}}(\mathsf{Rel}_{\mathit{Ka}}(O))$. By
definition, $\mathsf{ren}_{\mathit{Ka}}$ is injective so there exists an
inverse function
$\mathsf{ren}_{\mathit{Ka}}^{-}:\mathsf{ren}_{\mathit{Ka}}(\mathsf{N}^{\mathsf{nc}})\to\mathsf{N}^{\mathsf{nc}}$
which is itself injective, so that renaming terms
$t\in\mathsf{Sig}(\mathsf{ren}_{\mathit{Ka}}(\mathsf{Rel}_{\mathit{Ka}}(O)))\cap\mathsf{ren}(\mathsf{N}^{\mathsf{nc}})$
by $\mathsf{ren}_{\mathit{Ka}}^{-}(t)$ gives us a model
$\mathcal{I}^{\prime}=\langle\Delta^{\mathcal{I}},\cdot^{\mathcal{I}^{\prime}}\rangle$
of ontology $\mathsf{Rel}_{\mathit{Ka}}(O)$ where
$\mathsf{ren}_{\mathit{Ka}}^{-}(t)^{\mathcal{I}^{\prime}}=t^{\mathcal{I}}$ for
all
$t\in\mathsf{Sig}(\mathsf{ren}_{\mathit{Ka}}(\mathsf{Rel}_{\mathit{Ka}}(O)))$.

From $\mathcal{I}^{\prime}$, we can define another interpretation
$\mathcal{I}^{\prime\prime}=\langle\top_{\mathit{Ka}}^{\mathcal{I}},\cdot^{\mathcal{I}^{\prime}}\rangle$.
For this to be a valid interpretation, all individuals must be interpreted as
elements of $\top_{\mathit{Ka}}^{\mathcal{I}}$, all concepts must interpreted
as subsets of $\top_{\mathit{Ka}}^{\mathcal{I}}$, and all roles must be
interpreted as subsets of
$\top_{\mathit{Ka}}^{\mathcal{I}}\times\top_{\mathit{Ka}}^{\mathcal{I}}$. But
this is necessarily the case because the interpretation function is that of
$\mathcal{I}^{\prime}$, and $\mathcal{I}^{\prime}$ is a model of
$\mathsf{Rel}_{\mathit{Ka}}(O)$ where the axioms of Item 7 in Def. 9 guarantee
this property.

Now, we prove that
$\mathcal{I}^{\prime\prime}\models\mathsf{Rel}_{\mathit{Ka}}(O)$. Indeed, as
explained before, axioms added by Item 7 are satisfied. Then, it can be
checked by structural induction that for all concepts or roles $X$,
$\mathsf{rel}_{\mathit{Ka}}(X)^{\mathcal{I}^{\prime\prime}}=\mathsf{rel}_{\mathit{Ka}}(X)^{\mathcal{I}^{\prime}}$.
Moreover, all remaining axioms in $\mathsf{Rel}_{\mathit{Ka}}(O)$ (other than
those from $Item~{}\ref{itm:extra}$) are the result of applying the
relativization function on concepts and roles. Thus, all axioms of
$\mathsf{Rel}_{\mathit{Ka}}(O)$ are of one of the following forms:
$\mathsf{rel}_{\mathit{Ka}}(X)\sqsubseteq\mathsf{rel}_{\mathit{Ka}}(Y)$,
$\mathsf{rel}_{\mathit{Ka}}(C)(x)$, or $\mathsf{rel}_{\mathit{Ka}}(R)(x,y)$,
for $X,Y$ two concepts or two roles, $C$ a concept, $R$ a role, and $x,y$ two
individuals. Since $\mathcal{I}^{\prime}$ is a model of
$\mathsf{Rel}_{\mathit{Ka}}(O)$, if $C\sqsubseteq D\in\mathsf{Ax}(O)$, then
$\mathcal{I}^{\prime}\models\mathsf{rel}_{\mathit{Ka}}(C)\sqsubseteq\mathsf{rel}_{\mathit{Ka}}(D)$.
This, combined with the equality of
$\mathsf{rel}_{\mathit{Ka}}(X)^{\mathcal{I}^{\prime\prime}}$ and
$\mathsf{rel}_{\mathit{Ka}}(X)^{\mathcal{I}^{\prime}}$ for any concept or role
$X$, ensures that
$\mathcal{I}^{\prime\prime}\models\mathsf{rel}_{\mathit{Ka}}(C)\sqsubseteq\mathsf{rel}_{\mathit{Ka}}(D)$.
The same line of reasoning holds for $C(x)\in\mathsf{Ax}(O)$ and
$R(x,y)\in\mathsf{Ax}(O)$. It follows that
$\mathcal{I}^{\prime\prime}\models\mathsf{Rel}_{\mathit{Ka}}(O)$.

We finish the proof by showing that $\mathcal{I}^{\prime\prime}\models O$,
which proves that $O$ is consistent. Since
$\top^{\mathcal{I}^{\prime\prime}}=\top_{\mathit{Ka}}^{\mathcal{I}^{\prime\prime}}$,
adding $\sqcap\top_{\mathit{Ka}}$ to a concept does not change its
interpretation, and replacing $\top$ with $\top_{\mathit{Ka}}$ has no effect
on the interpretation of the concepts or roles. Consequently, for all concepts
or roles $X$,
$X^{\mathcal{I}^{\prime\prime}}=\mathsf{rel}_{\mathit{Ka}}(X)^{\mathcal{I}^{\prime\prime}}$.
Thus, when
$\mathcal{I}^{\prime\prime}\models\mathsf{Rel}_{\mathit{Ka}}(\alpha)$ it also
satisfies $\alpha$ and therefore, $\mathcal{I}^{\prime\prime}\models O$. ∎

###  4.4 Inference Preservation

In [15], we were only able to study entailment preservation in the limited
setting of $pD*$ entailment. Here we prove a much stronger theorem for
NdTerms. As in the two previous subsections, we fix a contextual annotation
$\mathit{Ka}$ that has its signature in $\mathsf{N}^{\mathsf{nc}}$.

######  Theorem 4.5 (Entailment preservation of NdTerms)

Let $\Omega$ be a set of ontologies having their signatures in
$\mathsf{N}^{\mathsf{nc}}$ and disjoint from the signature of $\mathit{Ka}$.
If $\mathit{Ka}$ is model extensible, then NdTerms is entailment preserving
for $\\{\langle O,\mathit{Ka}\rangle\\}_{O\in\Omega}$.

In order to prove this theorem, we must show that relativization preserves
entailments.

###### Lemma 2

Let $O_{1}$ and $O_{2}$ be two ontologies. If $O_{1}\models O_{2}$ then
$\mathsf{Rel}_{\mathit{Ka}}(O_{1})\models\mathsf{Rel}_{\mathit{Ka}}(O_{2})$.

######  Proof (Lemma 2)

Let $O_{1}$ and $O_{2}$ such that $O_{1}\models O_{2}$. If
$\mathsf{Rel}_{\mathit{Ka}}(O_{1})$ is inconsistent, then the property is
obviously verified. Otherwise, there exists a model
$\mathcal{I}=\langle\Delta^{\mathcal{I}},\cdot^{\mathcal{I}}\rangle$ of
$\mathsf{Rel}_{\mathit{Ka}}(O_{1})$. Using the same arguments as in the proof
of Theorem 4.4,
$\mathcal{I}^{\prime}=\langle\top_{\mathit{Ka}},\cdot^{\mathcal{I}}\rangle$ is
also a model of $\mathsf{Rel}_{\mathit{Ka}}(O_{1})$ and $\mathcal{I}^{\prime}$
interprets concepts and roles equally to their relativized counterparts, i.e.,
$X^{\mathcal{I}^{\prime}}=\mathsf{rel}_{\mathit{Ka}}(X)^{\mathcal{I}^{\prime}}$.
It follows that $\mathcal{I}^{\prime}\models O_{1}$ and since $O_{1}\models
O_{2}$, $\mathcal{I}^{\prime}\models O_{2}$, and
$\mathcal{I}^{\prime}\models\mathsf{Rel}_{\mathit{Ka}}(O_{2})$. By Theorem
4.3, we know that $\mathcal{I}^{\prime}$ is domain extensible for
$\mathsf{Rel}_{\mathit{Ka}}(O_{2})$. Consequently, $\mathcal{I}$ is also a
model of $\mathsf{Rel}_{\mathit{Ka}}(O_{2})$. ∎

With the lemma proven, we then prove Theorem 4.5.

######  Proof (Theorem 4.5)

Let us assume that $\mathit{Ka}$ is model extensible. Let $O_{1}$ and $O_{2}$
be two ontologies having their signatures in $\mathsf{N}^{\mathsf{nc}}$ and
disjoint from $\mathsf{Sig}(\mathit{Ka})$, such that $O_{1}\models O_{2}$. If
$f(\langle O_{1},\mathit{Ka}\rangle)$ is inconsistent, then the entailment is
trivially preserved. Otherwise, there exists a model
$\mathcal{I}=\langle\Delta^{\mathcal{I}},\cdot^{\mathcal{I}}\rangle$ of
$f(\langle O_{1},\mathit{Ka}\rangle)$. By definition of $f$, it satisfies
$\mathsf{ren}_{\mathit{Ka}}(\mathsf{Rel}_{\mathit{Ka}}(O_{1})$. Due to Lemma
2, $O_{1}\models O_{2}$ implies that
$\mathsf{Rel}_{\mathit{Ka}}(O_{1})\models\mathsf{Rel}_{\mathit{Ka}}(O_{2})$.
Moreover, using the fact that $\mathsf{ren}_{\mathit{Ka}}$ is just a renaming
of terms, and considering that “truth is invariant under change of notation”
[19], we know that
$\mathsf{ren}_{\mathit{Ka}}(O)\models\mathsf{ren}_{\mathit{Ka}}(O^{\prime})$
is equivalent to $O\models O^{\prime}$. Therefore,
$\mathsf{ren}_{\mathit{Ka}}(\mathsf{Rel}_{\mathit{Ka}}(O_{1})\models\mathsf{ren}_{\mathit{Ka}}(\mathsf{Rel}_{\mathit{Ka}}(O_{2})$.
Moreover, all axioms in $\mathsf{Cx}(\mathit{Ka})$ are satisfied by
$\mathcal{I}$. Finally, for $O_{2}$ to be entailed by $O_{1}$, the signature
of $O_{2}$ must be included in the signature of $O_{1}$. As a result, whenever
$\mathtt{isContextualPartOf}(\mathsf{ren}_{\mathit{Ka}},t)$ or
$\mathtt{isInContext}(\mathsf{ren}_{\mathit{Ka}}(t),\mathfrak{A}(\mathit{Ka}))$
are in $f(\langle O_{2},\mathit{Ka}\rangle)$, then they are in $f(\langle
O_{1},\mathit{Ka}\rangle)$ as well. Consequently, $f(\langle
O_{1},\mathit{Ka}\rangle)\models f(\langle O_{2},\mathit{Ka}\rangle)$. ∎

##  5 Annotations in Multiple Contexts

So far, we assumed that all axioms of an ontology are annotated with the same
contextual information. In this setting, the core of the contextualization
function in NdTerms amounts to relativizing the axioms and renaming the terms.
The renaming part may seem surprising because, as we said a couple of times
already, “truth is invariant under change of notation”. However, the
usefulness of the renaming part becomes apparent when we want to combine
several annotated ontologies having different contextual annotations (say
$\mathit{Ca}_{1}$ and $\mathit{Ca}_{2}$). In this case, if the renaming
functions $\mathsf{ren}_{\mathit{Ca}_{1}}$ and
$\mathsf{ren}_{\mathit{Ca}_{2}}$ are mapping non contextual terms into
disjoint sets of contextual terms, then the contextualization function
$f_{\mathsf{nd}}$ ensures that any inference made in a context will not
interact with the knowledge from another context. This avoids the
contextualized knowledge to be inconsistent when combining statements in
different contexts that contradict each others.

The properties presented in Sec. 3 require a little adaptation when applied to
the multi-contextual setting. Indeed, in spite of the soundness theorem of
Sec. 4.2, in the general case if a set of annotated ontologies $\\{\langle
O_{i},\mathit{Ca}_{i}\rangle\\}_{i\in I}$ are satisfying the constraints of
Theorem 4.1, it is still possible that $\bigcup_{i\in
I}f_{\mathsf{nd}}(\langle O_{i},\mathit{Ca}_{i}\rangle)$ is inconsistent. We
expect that the preservation of consistency can be guaranteed if _all_ the
signatures of $\\{O_{i}\\}$ are disjoint from _all_ the signatures of
$\\{\mathit{Ca}_{i}\\}$. Studying in more details the case of multiple
contextual annotations is planned for future work.

##  6 Other Approaches

Here we briefly present the most relevant reification approaches in the
Semantic Web. For all of them, the contextualization only annotates the role
assertions, leaving other axioms unmodified.

As seen in Ex. 4, _RDF reification_ replaces $\alpha=R(x,y)$ with three new
role assertions $\mathtt{subject}(\mathbf{a}_{\alpha}^{\mathit{Ca}},x)$,
$\mathtt{predicate}(\mathbf{a}_{\alpha}^{\mathit{Ca}},R)$, and
$\mathtt{object}(\mathbf{a}_{\alpha}^{\mathit{Ca}},y)$ and the axioms in the
contextual annotation are anchored on $\mathbf{a}_{\alpha}^{\mathit{Ca}}$,
which depends on the role assertion $R$ and the contextual annotation
$\mathit{Ca}$. As shown in Ex. 6 and 7, this contextualization method
preserves neither inconsistencies (in the sense of Def. 7) nor entailments on
role assertions.

###### Example 10

An _RDF reification_ contextualization of our running example within the
context $\mathit{CA}$ of Ex. 2 contains the following axioms:

$\mathtt{subject}(\mathtt{stbcobe},\mathtt{babylon})$

$\mathtt{predicate}(\mathtt{stbcobe},\mathtt{capital})$

$\mathtt{object}(\mathtt{stbcobe},\mathtt{babylonianEmpire})$

$\mathtt{validity}(\mathtt{stbcobe},\mathtt{t})$

$\mathtt{Interval}(\mathtt{t})$

$\mathtt{from}(\mathtt{t},\mathtt{609BC})$

$\mathtt{to}(\mathtt{t},\mathtt{539BC})$

$\mathtt{prov}(\mathtt{stbcobe,\mathtt{w}})$

$\mathtt{name}(\mathtt{w},\mathtt{wikipedia})$

$\mathtt{Wiki}(\mathtt{w})$

_N-Ary relations_ replaces $R(x,y)$ by two role assertions
$p_{1}(R)(x,\mathbf{a}_{\alpha}^{\mathit{Ca}})$ and
$p_{2}(R)(\mathbf{a}_{\alpha}^{\mathit{Ca}},y)$, where $R$ is a simple role
assertion, and $p_{1}$ and $p_{2}$ are two injective functions with disjoint
ranges that map non-contextual roles to contextual roles. Alternatively, a new
concept $C_{R}$ is added for the role $R$, and the following assertions are
added: $C_{R}(\mathbf{a}_{\alpha}^{\mathit{Ca}})$,
$p_{1}(R)(\mathbf{a}_{\alpha}^{\mathit{Ca}},x)$, and
$p_{2}(R)(\mathbf{a}_{\alpha}^{\mathit{Ca}},y)$.

###### Example 11

An _N-Ary relations_ contextualization of our running example within the
context $\mathit{CA}$ of Ex. 2 contains the following axioms:

$\mathtt{capitalOf\\#1}(\mathtt{babylon},\mathtt{rbcobe})$

$\mathtt{capitalOf\\#2}(\mathtt{rbcobe},\mathtt{babylonianEmpire})$

$\mathtt{validity}(\mathtt{rbcobe},\mathtt{t})$

$\mathtt{Interval}(\mathtt{t})$

$\mathtt{from}(\mathtt{t},\mathtt{609BC})$

$\mathtt{to}(\mathtt{t},\mathtt{539BC})$

$\mathtt{prov}(\mathtt{rbcobe,\mathtt{w}}$

$\mathtt{name}(\mathtt{w},\mathtt{wikipedia})$

$\mathtt{Wiki}(\mathtt{w})$

_Singleton property_ is using a non-standard semantics of RDF but the same
idea can be simulated with DL axioms. For each simple role axiom $R(x,y)$, the
following axioms are added: $\mathbf{a}_{\alpha}^{\mathit{Ca}}(x,y)$ (that is,
the term for the anchor is used as a role),
$\\{x\\}\equiv\exists\mathbf{a}_{\alpha}^{\mathit{Ca}}.\\{y\\}$ (which
guarantees that the anchor property is a singleton), and
$\mathtt{singletonPropertyOf}(\mathbf{a}_{\alpha}^{\mathit{Ca}},R)$.

###### Example 12

A _Singleton Property_ contextualization of our running example within the
context $\mathit{CA}$ of Ex. 2 contains the following axioms:

$\mathtt{capital\\#1}(\mathtt{babylon},\mathtt{babylonianEmpire})$

$\mathtt{singletonPropertyOf}(\mathtt{capital\\#1},\mathtt{capital})$

$\mathtt{validity}(\mathtt{capital\\#1},\mathtt{t})$

$\mathtt{Interval}(\mathtt{t})$

$\mathtt{from}(\mathtt{t},\mathtt{609BC})$

$\mathtt{to}(\mathtt{t},\mathtt{539BC})$

$\mathtt{prov}(\mathtt{capital\\#1,\mathtt{w}}$

$\mathtt{name}(\mathtt{w},\mathtt{wikipedia})$

$\mathtt{Wiki}(\mathtt{w})$

The remaining approach, _NdFluents_ , uses a similar approach as NdTerms
except that it only renames the terms used as individuals and does not
relativize the ontology. This ensures interesting properties wrt entailment
preservation [15], but TBox axioms in different contexts are not
distinguishable.

##  7 Discussion and Future Work

NdTerms and NdFluents are a concrete instantiations of a general approach of
contextualizing (parts of) the terms in the ontology. Other instantiations
would be possible, such as contextualizing role names (in a similar fashion as
the singleton property), class names, or a combination of them. Then, NdTerms
would be the approach where each and every term is contextualized, while in
NdFluents only individuals are.

In the future, we would like to deepen the analysis of contextualization,
filling gaps still present in this preliminary work. Especially, the
combination of multiple annotations, or annotations of contextualized
ontologies, present some interesting challenges. A more systematic comparison
of the various approaches remains to be presented.

#### Acknowledgement:

This work was partly funded by project WDAqua (H2020-MSCA-ITN-2014 #64279) and
project OpenSensingCity (ANR-14-CE24-0029).

## References

  * [1] McCarthy, J.L.:  Generality in Artificial Intelligence.  Communications of the ACM 30(12) (1987) 1029–1035
  * [2] Giunchiglia, F.:  Contextual Reasoning.  Epistemologica 16 (1993) 345–364
  * [3] Ghidini, C., Serafini, L.:  Distributed First Order Logics.  In Gabbay, D.M., de Rijke, M., eds.: Frontiers of Combining Systems 2\. Volume 7 of Studies in Logic and Computation., Research Studies Press (2000) 121–139
  * [4] Zimmermann, A.:  Logical formalisms for Agreement Technologies.  In Ossowski, S., ed.: Agreement Technologies.  Springer (2013)
  * [5] Kifer, M., Subrahmanian, V.S.:  Theory of generalized annotated logic programming and its applications.  Journal of Logic Programming 12(3&4) (1992) 335–367
  * [6] Udrea, O., Recupero, D.R., Subrahmanian, V.S.:  Annotated RDF.  ACM Transaction on Computational Logics 11(2) (2010)
  * [7] Zimmermann, A., Lopes, N., Polleres, A., Straccia, U.:  A general framework for representing, reasoning and querying with annotated Semantic Web data.  Journal of Web Semantics 11 (2012) 72–95
  * [8] Carroll, J.J., Bizer, C., Hayes, P., Stickler, P.:  Named graphs, provenance and trust.  In Ellis, A., Hagino, T., eds.: Proceedings of the 14th International Conference on World Wide Web, WWW 2005, Chiba, Japan, May 10-14, 2005, ACM Press (May 2007) 613–622
  * [9] Dividino, R.Q., Sizof, S., Staab, S., Schueler, B.:  Querying for provenance, trust, uncertainty and other meta knowledge in RDF.  Journal of Web Semantics 7(3) (2009) 204–219
  * [10] Hartig, O., Thompson, B.:  Foundations of an Alternative Approach to Reification in RDF.  CoRR abs/1406.3399 (2014)
  * [11] Hoffart, J., Suchanek, F.M., Berberich, K., Weikum, G.:  YAGO2: A spatially and temporally enhanced knowledge base from Wikipedia.  Artificial Intelligence 194 (2013) 28–61
  * [12] Brickley, D., Guha, R.V.:  RDF Schema 1.1, W3C Recommendation 25 February 2014.  W3C Recommendation, World Wide Web Consortium (February 25 2014)
  * [13] Noy, N.F., Rector, A.L.:  Defining N-ary Relations on the Semantic Web, W3C Working Group Note 12 April 2006.  W3C Note, World Wide Web Consortium (April 12 2006)
  * [14] Nguyen, V., Bodenreider, O., Sheth, A.:  Don’t like RDF reification?: making statements about statements using singleton property.  In Chung, C.W., Broder, A.Z., Shim, K., Suel, T., eds.: 23rd International World Wide Web Conference, WWW ’14, Seoul, Republic of Korea, April 7-11, 2014, ACM Press (April 2014) 759–770
  * [15] Giménez-García, J.M., Zimmermann, A., Maret, P.:  NdFluents: An Ontology for Annotated Statements with Inference Preservation.  In Blomqvist, E., Maynard, D., Gangemi, A., Hoekstra, R., Hitzler, P., Hartig, O., eds.: The Semantic Web - 14th International Conference, ESWC 2017, Portorož, Slovenia, May 28 - June 1, 2017, Proceedings, Part I. Volume 10249 of Lecture Notes in Computer Science., Springer (May 2017) 638–654
  * [16] Golbreich, C., Wallace, E.K.:  OWL 2 Web Ontology Language, New Features and Rationale (Second Edition), W3C Recommendation 11 December 2012.  W3C Recommendation, World Wide Web Consortium (December 11 2012)
  * [17] Scott, D.S.:  Identity and existence in intuitionalistic logic.  In Fourman, M., Mulvay, C., Scott, D.S., eds.: Applications of Sheaves, Proceedings of the Research Symposium on Applications of Sheaf Theory to Logic, Algebra, and Analysis, Durham, July 9-21, 1977. Volume 753 of Lecture Notes in Mathematics., Springer (1979) 660–696
  * [18] Cuenca-Grau, B., Kutz, O.:  Modular Ontology Languages Revisisted.  In Honavar, V.G., Finin, T.W., Caragea, D., Mladenic, D., Sure, Y., eds.: SWeCKa 2007: Proceedings of the IJCAI-2007 Workshop on Semantic Web for Collaborative Knowledge Acquisition, Hyderabad, India, January 7, 2007. (January 2007)
  * [19] Goguen, J.A., Burstall, R.M.:  Institutions: Abstract Model Theory for Specification and Programming.  Journal of the ACM 39(1) (1992) 95–146