is also $\oplus$-idempotent) is $\sf{PosBool}[{\sf X}]$, and the universal
semiring for idempotent semirings such that $\oplus\approx\otimes$ is
$\sf{Lin}[{\sf X}]$.

As in the preceding section, since we always consider $\sf{PosBool}[{\sf
X}]$\- or $\sf{Lin}[{\sf X}]$-annotated ontologies, we often omit the
superscripts $\sf{PosBool}[{\sf X}]$ or $\sf{Lin}[{\sf X}]$ and let
$\mathcal{O}$ be an ontology annotated with an injective function
$\lambda_{\sf X}$ from the axioms in $\mathcal{O}$ to the set of variables
${\sf X}$.

###  5.1 $\sf{PosBool}[{\sf X}]$-Provenance

Intuitively, the absorptivity of $\sf{PosBool}[{\sf X}]$ means that extending
a monomial with more elements is superfluous, as the resulting polynomial will
remain unchanged. Hence, provenance in the $\sf{PosBool}[{\sf X}]$ semiring
corresponds to the task of finding the _minimal_ monomials that occur in the
$\sf{Why}[{\sf X}]$-provenance of a consequence. The name arises from the fact
that $\sf{PosBool}[{\sf X}]$ corresponds to the lattice of all positive
Boolean formulas over the set ${\sf X}$ of variables (modulo propositional
equivalence). In this context, the semiring product is the propositional
conjunction $\land$ and the addition is the disjunction $\lor$.

####  5.1.1 Relationship with Axiom Pinpointing

Provenance over the $\sf{PosBool}[{\sf X}]$ semiring has been thoroughly
studied in the DL literature under the name of _axiom pinpointing_ (originally
coined by ? (?)). In this context, the goal is to find one or all the
_minimal_ (w.r.t. set inclusion) subsets of axioms that entail a given
consequence. These sets are called the _justifications_ for the consequence
(?). This definition of justifications can be straightforwardly extended to
justifications for BCQs. The connection between justifications and provenance
is easily observed by representing each set as the monomial formed by the
product of its element annotations and a class of sets as the addition of
their corresponding monomials. This construction has also been called the
_pinpointing formula_ in the DL literature (?). Importantly, monotonicity of
description logics ensures that every superset of a justification also entails
the consequence, which corresponds to the absorption in $\sf{PosBool}[{\sf
X}]$.

######  Proposition 5.1.

Let $\mathcal{O}$ be a satisfiable $\sf{PosBool}[{\sf X}]$-annotated ${\cal
E\\!LHI}_{\bot}$ ontology. For every BCQ or axiom $\alpha$ which is not a
concept or role inclusion whose left-hand side is unsatisfiable w.r.t.
$\mathcal{O}$, if ${\sf Just_{\mathcal{O}}}(\alpha)$ denotes the set of all
justifications for $\alpha$ w.r.t. $\mathcal{O}$, then

$\mathcal{P}(\alpha,\mathcal{O})=\bigvee_{\mathcal{J}\in{\sf
Just_{\mathcal{O}}}(\alpha)}\ \bigwedge_{\beta\in\mathcal{J}}\lambda_{\sf
X}(\beta).$

###### Proof.

By definition of $\sf{PosBool}[{\sf X}]$, we have that
$\mathcal{P}(\alpha,\mathcal{O})=\bigvee_{\mathcal{M}\subseteq\mathcal{O},\mathcal{M}\models\alpha}\bigwedge_{\beta\in\mathcal{M}}\lambda_{\sf
X}(\beta)$. Take an arbitary $\mathcal{M}\subseteq\mathcal{O}$ such that
$\mathcal{M}\models\alpha$. If this set is not a justification, then there
exists a subset $\mathcal{J}\subseteq\mathcal{M}$ which is a justification,
and hence also satisfies $\mathcal{J}\models\alpha$. By absorption, it follows
that $\mathcal{P}(\alpha,\mathcal{O})=\bigvee_{\mathcal{J}\in{\sf
Just_{\mathcal{O}}}(\alpha)}\bigwedge_{\beta\in\mathcal{J}}\lambda_{\sf
X}(\beta)$. ∎

######  Remark 5.2.

As in Proposition 4.1, the condition on $\alpha$ comes from the fact that for
GCI or role inclusion with an unsatisfiable left-hand side,
$\mathcal{O}^{\sf{PosBool}[{\sf X}]}\models(\alpha,\kappa)$ for every
$\kappa\in\sf{PosBool}[{\sf X}]$ (cf. Remark 3.2). If
$\mathcal{O}=\\{(A\sqsubseteq\neg B,v_{1}),(C\sqsubseteq
A,v_{2}),(C\sqsubseteq B,v_{3})\\}$, then for every $D\in{\sf N_{C}}$,
$\mathcal{O}\models C\sqsubseteq D$ and the only justification for
$\mathcal{O}\models C\sqsubseteq D$ is $\mathcal{O}$ itself. However,
$\mathcal{P}(\alpha,\mathcal{O})$ is the sum over all elements of
$\sf{PosBool}[{\sf X}]$ so is equal to 1.

In the context of axiom pinpointing, it is common to allow for static axioms
to capture cases where, for instance, the assertions or the GCIs and RIs are
considered to be immutable, among many other situations that appear in
different formalisms (?, ?, ?). Formally, we consider that a DL ontology
$\mathcal{O}$ is partitioned into two subsets
$\mathcal{O}:=\mathcal{O}_{s}\cup\mathcal{O}_{r}$ where $\mathcal{O}_{s}$ is
the class of _static_ axioms, which are assumed to always hold, and
$\mathcal{O}_{r}$ is the class of _refutable_ axioms which take part in the
justifications. In particular, to the best of our knowledge, the only
systematic study on the computation of BCQ justifications considers
justifications to be sets of assertions, i.e. GCIs and RIs to be static (?).
To handle this case, we may simply compute the $\sf{PosBool}[{\sf
X}]$-provenance and consider the semiring homomorphism that maps $\lambda_{\sf
X}(\beta)$ to 1 for every $\beta\in\mathcal{O}_{s}$.

It is worth noting that the problem of axiom pinpointing has been studied,
under different names, in many other communities like—among many
others—propositional satisfiability (?), process modelling (?), and answer set
programming (?).

####  5.1.2 Computing $\sf{PosBool}[{\sf X}]$-Provenance

There exist two main approaches for finding and enumerating the justifications
for a given consequence of an ontology. The _black-box_ approach simply calls
an existing (classical) reasoner repeatedly to prune out superfluous axioms
(?); the _glass-box_ approach, on the other hand, modifies the reasoner to
compute the justifications directly. The specific glass-box technique needed
obviously depends on the characteristics of the underlying reasoner, but
general frameworks have been developed for tableaux (?), automata (?), and
consequence-based (?) methods. Within the context of ${\cal E\\!LHI}_{\bot}$,
it has also been proposed to reduce the problem to an enumeration in SAT (?,
?, ?) or ASP (?, ?).

Since $\sf{PosBool}[{\sf X}]$-provenance can be obtained from $\sf{Why}[{\sf
X}]$-provenance by removing the non-minimal monomials, the algorithms we gave
in Section 4 provides a glass-box approach to compute the set of all
justifications for an axiom or a BCQ in ${\cal E\\!LHI}_{\bot}$. This is in
particular interesting for BCQs for which the problem of finding all
justifications that take into account axioms beyond assertions has not been
considered yet.

A direct consequence of the black-box methods is that one justification can be
computed (or verified) with a polynomial number of calls to a classical
reasoner. This means that a justification in ${\cal E\\!LHI}_{\bot}$ can be
found in exponential time, and this bound reduces to polynomial time in any
sublogic of ${\cal E\\!LHI}_{\bot}$ which allows for polynomial-time
reasoning. On the other hand, it is known that a single consequence may have
exponentially many justifications (?). This means that enumerating all
justifications (that is, finding the full $\sf{PosBool}[{\sf X}]$-provenance
polynomial in extended form) necessarily requires exponential time. Through a
more fine-grained complexity analysis, ? (?) showed that the computation of
all justifications for ${\cal E\\!L}$ consequences is super-polynomial on the
number of justifications. In a nutshell, this means that there exists no
algorithm that can compute all justifications in polynomial time _even if only
polynomially many justifications exist_. Yet, one can still compute a compact
representation of all the justifications—exploiting structure sharing and the
distributivity of $\sf{PosBool}[{\sf X}]$—in polynomial time.

####  5.1.3 Special Cases and Applications

Every distributive lattice and by extension every total ordering with the
$\min$ and $\max$ operators forms an absorptive, idempotent semiring. This
means that the techniques developed for axiom pinpointing can be directly
applied to any setting based on distributive lattices. To compute the
provenance of a consequence, one can simply compute the supremum (over the
lattice) of the infimum of the values of all the elements in a justification.
Formally, the provenance of an axiom or query $\alpha$ is
$\sup_{\mathcal{J}\in{\sf
Just_{\mathcal{O}}}(\alpha)}\inf_{\beta\in\mathcal{J}}\lambda(\beta),$ where
$\lambda$ is the annotation function that assigns a lattice value to each
axiom. For instance, ? (?) use an optimised variant of the axiom pinpointing
algorithm to compute access level and to suggest changes to correct it (?).
Another special case of this setting is the fuzzy semiring $\mathbb{F}$ which
naturally forms an infinite total ordering over $[0,1]$. As mentioned earlier,
the fuzzy degree of a consequence $\alpha$ corresponds to the minimum degree
that all the axioms in a subontology entailing $\alpha$ must have. Indeed, the
$n$-cuts from Section 3.3 are an efficient way to approximate the infima of
justifications, by allowing some superfluous axioms that do not interfere with
the overall result.

Dealing with the $\sf{PosBool}[{\sf X}]$ semiring has also proven to be useful
to define other semantics where one might not be interested in all the
possible derivations of a consequence (as in provenance in general), but only
on a limited class of them. This is the case for probabilistic databases (?)
and some probabilistic DLs based on the multiple-world semantics (?, ?). At
first sight, these can be treated directly with the probability semiring
$(\mathbb{R}_{+},+,\times,0,1)$. However, the semantics of this setting
requires that, when an axiom (or data element) is used more than once, its
probability should not be multiplied repeatedly. In practical terms, this
means that one should apply the semiring operations only over the _sets_ of
axioms that entail the consequence, and not through the derivation operation,
i.e. use the probability semiring operations in the formula
$\bigoplus_{\mathcal{J}\in{\sf
Just_{\mathcal{O}}}(\alpha)}\bigotimes_{\beta\in\mathcal{J}}\lambda(\beta)$. A
similar setting—in which a non-idempotent semiring is applied on the
$\sf{PosBool}[{\sf X}]$ provenance formula—has also been used in the context
of probabilistic logic programming, for parameter learning in ProbLog (?, ?),
using the gradient semiring
$(\mathbb{R}_{+}\times\mathbb{R}^{d},\oplus,\otimes,(0,\vec{0}),(1,\vec{0}))$,
where
$(a_{1},\vec{a_{2}})\oplus(b_{1},\vec{b_{2}})=(a_{1}+b_{1},\vec{a_{2}}+\vec{b_{2}})$
and
$(a_{1},\vec{a_{2}})\otimes(b_{1},\vec{b_{2}})=(a_{1}b_{1},b_{1}\vec{a_{2}}+a_{1}\vec{b_{2}})$
(the gradient semiring was originally called the _expectation_ semiring (?)).

###  5.2 $\sf{Lin}[{\sf X}]$-Provenance

Recall that $\sf{Lin}[{\sf X}]$ is the universal provenance semiring for
idempotent semirings such that $\oplus\approx\otimes$. In the database
setting, it associates to queries their lineage, or set of contributing facts.
Formally, $\sf{Lin}[{\sf X}]=({\sf
X}^{2}\cup\\{\emptyset^{*}\\},\cup,\cup^{*},\emptyset^{*},\emptyset)$ where
$\emptyset^{*}\cup S=S\cup\emptyset^{*}=S$,
$\emptyset^{*}\cup^{*}S=S\cup^{*}\emptyset^{*}=\emptyset^{*}$, and
$S_{1}\cup^{*}S_{2}=S_{1}\cup S_{2}$ if $S_{1},S_{2}\neq\emptyset^{*}$ (?). It
is well-known in the database setting that the lineage of a query can be
obtained by flattening its why-provenance, i.e. is the set of the variables
that occur in the why-provenance.

######  Proposition 5.3.

Let $\mathcal{O}$ be an ${\cal E\\!LHI}_{\bot}$ ontology annotated by
$\lambda_{\sf X}$. For every BCQ or axiom $\alpha$,
$\mathcal{P}(\alpha,\mathcal{O}^{\sf{Lin}[{\sf X}]})=\\{v\mid v\text{ occurs
in }\mathcal{P}(\alpha,\mathcal{O}^{\sf{Why}[{\sf X}]})\\}$.

###### Proof.

The case where $\mathcal{O}$ is unsatisfiable or $\alpha$ is a GCI/RI with an
unsatisfiable left-hand side follows directly from the definition of
$\mathcal{P}(\alpha,\mathcal{O}^{\sf{Lin}[{\sf X}]})$ and
$\mathcal{P}(\alpha,\mathcal{O}^{\sf{Why}[{\sf X}]})$, so we next assume that
we are not in such cases. Since the $\sf{Why}[{\sf X}]$ semiring specializes
correctly to $\sf{Lin}[{\sf X}]$, $h:\sf{Why}[{\sf X}]\rightarrow\sf{Lin}[{\sf
X}]$ defined by $h(v)=\\{v\\}$ for every $v\in{\sf X}$ extends uniquely to a
semiring homomorphism. Hence, by Theorem 3.28,

$\displaystyle\mathcal{P}(\alpha,\mathcal{O}^{\sf{Lin}[{\sf X}]})$
$\displaystyle=h(\mathcal{P}(\alpha,\mathcal{O}^{\sf{Why}[{\sf X}]}))$
$\displaystyle=h(\sum_{\mathcal{O}^{\sf{Why}[{\sf X}]}\models(\alpha,m)}m)$
$\displaystyle=\bigcup_{\mathcal{O}^{\sf{Why}[{\sf X}]}\models(\alpha,m)}h(m)$
$\displaystyle=\bigcup_{\mathcal{O}^{\sf{Why}[{\sf
X}]}\models(\alpha,m)}\bigcup_{\begin{subarray}{c}v\in{\sf X},\\\ v\text{
occurs in }m\end{subarray}}h(v)$ $\displaystyle=\\{v\mid v\text{ occurs in
}\mathcal{P}(\alpha,\mathcal{O}^{\sf{Why}[{\sf X}]})\\}.\qed$

Provenance in the $\sf{Lin}[{\sf X}]$ semiring allows us to answer the
question whether a given axiom occurs in some derivation of an axiom or a
query: we say that $v\in{\sf X}$ is _relevant_ for the entailment of an axiom
or BCQ $\alpha$ w.r.t. an ontology $\mathcal{O}$ annotated with variables from
${\sf X}$ iff $v\in\mathcal{P}(\alpha,\mathcal{O}^{\sf{Lin}[{\sf X}]})$. By
Proposition 5.3, $v$ is relevant for the entailment of $\alpha$ iff there
exists $m\in\mathsf{mon}({\sf X})$ such that $\mathcal{O}^{\sf{Why}[{\sf
X}]}\models(\alpha,v\times m)$.

####  5.2.1 Computing $\sf{Lin}[{\sf X}]$-Provenance of Axioms

We show that provenance in the $\sf{Lin}[{\sf X}]$ semiring for axiom
entailment can be computed via an adaptation of the completion algorithm
(Section 4.1) for computing the $\sf{Lin}[{\sf X}]$-provenance of all concept
and role assertions $A(a)$ or $R(a,b)$ with $a,b\in{\sf N_{I}}$, $A\in{\sf
N_{C}}$, $R\in{\sf N_{R}}$ by combining all monomials from a derivation,
instead of storing them separately. In particular, it will follow that if
$\mathcal{O}$ belongs to $\mathcal{ELHI_{\bot}^{\mathit{restr}}}$ (in
particular if $\mathcal{O}$ is in ${\cal E\\!LH}^{r}$ or DL-LiteR), provenance
in the $\sf{Lin}[{\sf X}]$ semiring can be computed in _polynomial time_.

As in Section 4.1, the algorithm assumes normal form and keeps as data
structure a set $\mathcal{S}$ of annotated axioms $(\alpha,m)$, where $\alpha$
uses the vocabulary of $\mathcal{O}$, and $m\in\mathsf{mon}({\sf X})$.
$\mathcal{S}$ is initialised as in Section 4.1 and extended by exhaustively
applying the rules in Table 2, where rule applications are modified to change
$\mathcal{S}$ into

$\mathcal{S}\Cup\\{(\alpha,m)\\}:=\begin{cases}\mathcal{S}\cup\\{(\alpha,m)\\}\text{
if there is no $(\alpha,n)\in\mathcal{S}$}\\\
\mathcal{S}\setminus\\{(\alpha,n)\\}\cup\\{(\alpha,m\times n)\\}\text{ if
$(\alpha,n)\in\mathcal{S}$;}\end{cases}$

i.e., add the axiom $\alpha$ with an associated monomial if it does not yet
appear in $\mathcal{S}$, and modify the monomial associated to $\alpha$ to
include new variables otherwise. The rules are applied until no new rule is
applicable; i.e., $\mathcal{S}$ is  _saturated_.

######  Example 5.4.

On the ontology of Example 4.10, we obtain the saturated set

$\displaystyle\mathcal{S}=$ $\displaystyle\\{(A\sqsubseteq A,m),(B\sqsubseteq
B,m),(A\sqsubseteq B,m),(B\sqsubseteq A,m)\\}\ \cup$
$\displaystyle\\{(A_{i}\sqsubseteq B,m),(B\sqsubseteq
A_{i},m),(A_{i}\sqsubseteq A,m),(A\sqsubseteq A_{i},m)\mid(1\leq i\leq n\\}\
\cup$ $\displaystyle\\{(A_{i}\sqsubseteq A_{j},m)\mid 1\leq i,j\leq n\\}$

with $m=u\times\Pi_{i=1}^{n}u_{i}\times\Pi_{i=1}^{n}v_{i}$. ∎

######  Theorem 5.5.

If $\mathcal{O}$ is a satisfiable $\sf{Lin}[{\sf X}]$-annotated ${\cal
E\\!LHI}_{\bot}$ ontology, $\alpha$ is an assertion s.t.
$\mathcal{O}\models\alpha$, and $\mathsf{linsat}(\mathcal{O})$ is the
saturated set obtained from $\mathcal{O}$, then
$(\alpha,\mathcal{P}(\alpha,\mathcal{O}))\in\mathsf{linsat}(\mathcal{O})$ and
there is no other $m$ such that $(\alpha,m)\in\mathsf{linsat}(\mathcal{O})$.

This yields an exponential-time upper bound for the problems of computing the
$\sf{Lin}[{\sf X}]$-provenance and deciding the relevance of an axiom for
assertion entailment in ${\cal E\\!LHI}_{\bot}$. As in Section 4.1, axioms can
be handled in exponential time as well. Moreover, we show that if
$\mathcal{O}$ belongs to $\mathcal{ELHI_{\bot}^{\mathit{restr}}}$, provenance
in the $\sf{Lin}[{\sf X}]$ semiring can be computed in polynomial time using
the completion rules modified for this case as in Theorem 4.11.

######  Theorem 5.6.

Let $\mathcal{O}$ be a satisfiable $\sf{Lin}[{\sf X}]$-annotated ${\cal
E\\!LHI}_{\bot}$ ontology, and $\alpha$ be an axiom.

  * •

$\mathcal{P}(\alpha,\mathcal{O})$ can be computed in exponential time w.r.t.
$|\mathcal{O}|$.

  * •

If $\mathcal{O}$ belongs to $\mathcal{ELHI_{\bot}^{\mathit{restr}}}$,
$\mathcal{P}(\alpha,\mathcal{O})$ can be computed in polynomial time w.r.t.
$|\mathcal{O}|$.

This result shows that if we only need to know which axioms are used to derive
an axiom, the complexity is the same as reasoning without provenance in ${\cal
E\\!LHI}_{\bot}$ and $\mathcal{ELHI_{\bot}^{\mathit{restr}}}$. This contrasts
with the axiom pinpointing setting in which deciding whether an axiom belongs
to a justification is NP-hard for Horn-${\cal E\\!L}$ (?). This is because
$\sf{Lin}[{\sf X}]$-provenance does not require _minimality_ : if
$\mathcal{O}=\\{(A\sqsubseteq B,v_{1}),(B\sqsubseteq C,v_{2}),(C\sqsubseteq
B,v_{3})\\}$, $\mathcal{P}(A\sqsubseteq
B,\mathcal{O})=\\{v_{1},v_{2},v_{3}\\}$ and in particular $v_{2}$ and $v_{3}$
are relevant for $A\sqsubseteq B$, but the only justification is
$\\{A\sqsubseteq B\\}$ so other axioms are not relevant for axiom pinpointing.

####  5.2.2 Relationship with Lean Kernels

Provenance in the $\sf{Lin}[{\sf X}]$ semiring is related to _lean kernels_
(?), which approximate the union of justifications. The lean kernel of a
consequence $\alpha$ (being an assertion or subsumption between two concept
names) is the set of axioms appearing in at least one proof of $\alpha$ in a
given inference method, generalizing the notion from propositional logic,
where a lean kernel is the set of clauses appearing in a resolution proof for
unsatisfiability. The sets of variables computed by our algorithm are the sets
of axioms used in the derivations by the completion algorithm, which is a
consequence-based method for ${\cal E\\!LHI}_{\bot}$. Thus they correspond to
lean kernels for the associated axioms and our algorithm is an alternative way
of computing lean kernels for assertions in ${\cal E\\!LHI}_{\bot}$.

##  6 Related Work on Provenance

In this section, we review and discuss some work on provenance, and in
particular semiring provenance, in various settings.

##### Provenance in relational databases

The research on provenance in relational databases has been extremely
flourishing (see, e.g. surveys and discussion papers by ? (?), ? (?), ? (?),
and ? (?)). Tracing the provenance of query result for explaining, debugging
or uncertainty handling has been an important topic of interest already before
the introduction of semiring provenance. For example, ? (?) introduced why-
and where-provenance, ? (?) implemented a notion of provenance corresponding
to $\sf{Trio}[{\sf X}]$ to handle uncertain data, and ? (?) showed that
deciding whether a given fact is part of the why or where provenance is
intractable. This result contrasts with the polynomial upper bound given in
Theorem 5.6 for computing the $\sf{Lin}[{\sf X}]$-provenance of axioms in
$\mathcal{ELHI_{\bot}^{\mathit{restr}}}$, and shows that it is not possible to
extend this result for BCQs. Semiring provenance introduced by ? (?) unify and
generalize many of these early works, using different provenance semirings (?,
?). There have been several attempts at extending semiring provenance for
relational databases to more expressive query languages, for example featuring
aggregation (?). In particular, non-monotone queries with difference attracted
interest: ? (?) proposed to use a monus operator on the underlying semiring,
and call m-semirings the class of semirings with such an operator, but ? (?)
show limitations of the approach. Similar questions will certainly arise if we
try to extend our framework to DLs or queries featuring negation. The case of
Boolean provenance ($\sf{PosBool}[{\sf X}]$) of non-monotone queries is
however well-understood (?). There exist a few systems for relational
provenance management such as Perm (?), GProM (?), and most notably ProvSQL
(?) which supports all provenance semirings, provenance semirings with monus,
and where-provenance, as well as arbitrary user-defined semirings, and has
been used by ? (?) to implement a provenance-aware ontology-based data access
system.

##### Provenance for Datalog queries

By Theorem 3.26, for commutative $\oplus$-idempotent $\omega$-continuous
semirings and ontologies whose GCIs have only concept names has right-hand
sides and RIs are positive, the provenance of any BCQ can be computed using
the tools developed for computing the provenance of Datalog queries over
databases, via the translation of the ontology and query to a Datalog program.
This is in particular true for the $\sf{Why}[{\sf X}]$-provenance and
$\sf{PosBool}[{\sf X}]$-provenance which have attracted a lot of interest in
the Datalog literature. Datalog provenance has been considered since the
seminal work on provenance by ? (?) who gave an algorithm for computing the
coefficient of a particular monomial in the provenance series of the query. ?
(?) study the data complexity of deciding whether a monomial is part of the
$\sf{Why}[{\sf X}]$-provenance for Datalog queries and show that while the
problem is in general intractable, it is tractable for non-recursive Datalog.
? (?) proposed circuit-based provenance representation as an efficient way to
compute provenance with absorptive (hence $\oplus$-idempotent) semirings
($\sf{Sorp}[{\sf X}]$-provenance) as well as $\sf{Why}[{\sf X}]$-provenance.
Several approaches have also been investigated to approximate Datalog
provenance. For example, ? (?) propose to compute a compact representation of
the top-k derivation trees, ranking the trees using tree patterns and facts
and rules they use. The implemented approaches either use these kinds of
approximations, restrict the language and/or constrain the semiring: ? (?)
consider only minimal depth proof trees computed through semi-naïve
evaluation; ? (?) use SQL to compute provenance of non-recursive Datalog
queries; ? (?) use a hypergraph that represents all derivation steps of the
Datalog program to compute the $\sf{Why}[{\sf X}]$-provenance either via a
system of equation or via a translation to an extension of Datalog with sets;
? (?) translate a Datalog program into a weighted hypergraph and characterize
the semirings where the best-weight derivation in the hypergraph corresponds
to the provenance for the initial Datalog program, and use this translation to
develop a practical approach to compute Datalog provenance in absorptive
semirings that are totally ordered; finally, ? (?) propose a practical SAT-
based approach for computing the $\sf{Why}[{\sf X}]$-provenance based on a
restricted class of proof-trees. ? (?) study the properties of such
alternative definitions of Datalog provenance based on subclasses of
derivation trees but also, more related to our work, based on annotated models
(cf. Lemma 3.27). Finally, ? (?) study the convergence of Datalog over
arbitrary (not necessarily $\omega$-continuous) partially ordered pre-
semiring, extending the provenance framework.

##### Provenance for the semantic web

Several works focus on querying annotated RDF data with SPARQL (?, ?). In
particular, ? (?) consider SPARQL queries on RDF data annotated with values
from some arbitrary annotation domain $K$ equipped with three binary
operations (with $\ominus$ to cover SPARQL difference operator) and show that
$(K,\oplus,\otimes,\ominus,0,1)$ must be an extension of semiring they called
spm-semiring and further study. As far as reasoning is concerned, ? (?)
defined an algebraic deductive system for RDFS annotated with elements of a
$\oplus$-idempotent semiring (not necessarily commutative), and ? (?) consider
RDFS annotated with elements of a $\oplus$-idempotent commutative semiring and
define a semantics based on annotated interpretations and a deductive system.
These two deductive systems are similar in spirit to our completion algorithm
for the $\sf{Why}[{\sf X}]$ semiring, the main difference being the existence
of a generalization rules that deduces $(\alpha,\kappa\oplus\kappa^{\prime})$
from $(\alpha,\kappa)$ and $(\alpha,\kappa^{\prime})$, while our completion
algorithm only computes the monomials that then need to be added to obtain the
full $\sf{Why}[{\sf X}]$-provenance, hence avoiding another blowup of the
saturated ontology.

##### Provenance in description logics

The closest work to ours is that presented by ? (?) and ? (?), which the
present paper revisits. We consider ${\cal E\\!LHI}_{\bot}$, which extends DL-
LiteR and ${\cal E\\!LH}^{r}$ that are considered by ? and ? respectively.
Moreover, we redefine the semantics to be more in line with the semiring
provenance framework and answer a lot of questions that were left implicit in
the previous papers: We study the properties of the semantics depending on the
properties of the semiring, and in particular show the relationship between
our semantics and the classical semiring provenance of relational or Datalog
queries. We also show how it captures (or does not capture) the semantics of
several annotated description logic such as fuzzy or possibilistic description
logic. Other kinds of provenance have also been considered for DL. ? (?)
define provenance in the expressive DL ${\cal ALC}$, considering only
annotated (complex) assertions. In this setting, the semantics is defined by
interpretations that map instance queries to elements of the semiring. The
authors focus on handling negation, and the semantics is defined so that
$(C(a),\kappa)$ and $(D(a),\kappa)$ (in our notation) follow from $((C\sqcap
D)(a),\kappa)$. Starting with instance queries and looking for a contradiction
using tableaux rules, provenance tokens of the original complex assertions are
propagated to their simpler consequences. In contrast, our approach proceeds
bottom-up and starts with simple assertions whose combinations lead to the
entailment of queries and traces their provenance combinations. ? (?)
considers GCIs entailment from expressive ontologies (with a focus on ${\cal
ALC}$) annotated with elements of a $\oplus$\- and $\otimes$-idempotent
commutative semiring. To handle ${\cal ALC}$ constructors, and in particular
negation, the author defines a provenance semantics based on interpretations
that do not satisfy the consequence. For each such interpretation, it takes
the sum of the labels of the ontology axioms violated by the interpretation,
then the provenance is defined as the product of these sums. When the semiring
is absorptive, this notion of provenance corresponds to $\sf{PosBool}[{\sf
X}]$-provenance, but when the semiring is not absorptive, the semantics
differs from the $\sf{Why}[{\sf X}]$-provenance. For example if we consider
the ontology $\\{(A\sqsubseteq B,\kappa),(C\sqsubseteq D,\kappa^{\prime})\\}$,
the provenance of $A\sqsubseteq B$ defined by ? is
$\kappa\otimes(\kappa\oplus\kappa^{\prime})=\kappa\oplus\kappa\otimes\kappa^{\prime}$,
while $C\sqsubseteq D$ is not relevant for the entailment of $A\sqsubseteq B$
in the sense of Section 5.2. Finally, the approach by ? (?) for attributed DL-
Lite fundamentally differs since it uses GCIs and RIs to express constraints
on provenance (for example by requiring that a premise of a GCI is entailed
from a given source to use this GCI) rather than tracking how axioms are
derived.

##### Provenance in other settings

Semiring provenance have been extended to many other settings. ? (?) define
the semiring provenance for a fragment of positive XQuery on XML annotated
with elements of commutative semirings. Semiring provenance for regular path
queries over graph databases has also been investigated (?, ?). Finally, a
recent line of research developed semiring provenance for very general logical
languages, such as first-order logic and fixed-point logic (?, ?). In this
context, interpretations associate a semiring element to literals (ground
facts and their negation) and are extended to more complex formula as
expected. This could be a track to explore to extend the semiring provenance
semantics to more expressive DLs, since it is not clear how to handle
disjunction and full negation in our framework.

##  7 Conclusions and Future Work

In this paper, we define a semiring provenance semantics for ${\cal
E\\!LHI}_{\bot}$ ontologies, more in line with the classical semiring
provenance for relational databases than previous proposals. After studying
its properties depending on the semiring characteristics, we focus on the case
of fully idempotent semirings, and provide algorithms and complexity results
for computing the $\sf{Why}[{\sf X}]$-provenance of axioms and conjunctive
queries. We also investigate in more details $\sf{PosBool}[{\sf
X}]$-provenance and $\sf{Lin}[{\sf X}]$-provenance and discuss connections
with notions related to explanations in description logics. Besides ${\cal
E\\!LHI}_{\bot}$, we also consider $\mathcal{ELHI_{\bot}^{\mathit{restr}}}$, a
fragment of ${\cal E\\!LHI}_{\bot}$ with the same good computational
complexity as DL-Lite and ${\cal E\\!L}$.

When one of the semiring operations is not idempotent, we have seen in Section
3.5 that our provenance semantics may exhibit some counter intuitive
behaviors. However, it may still be relevant to investigate it further in some
cases. For $\oplus$-idempotent semirings that are not $\otimes$-idempotent,
Theorem 3.19 does not hold and some concept subsumptions entailed by the
ontology may have an unexpected null provenance. It will nevertheless be
interesting to investigate the case where the TBox is not annotated, in
particular in the case of $\oplus$-idempotent, absorptive semirings
($\sf{Sorp}[{\sf X}]$ provenance) since it covers useful semirings such as the
Tropical semiring (costs), the Viterbi semiring (confidence) or the
Łukasiewicz semiring (truth values). When the addition is not idempotent,
Theorems 3.22, 3.24, 3.26 and 3.28 do not hold: the provenance of queries is
not in line with the one defined for relational databases or Datalog queries
in the database literature, and provenance expressions in a provenance
semiring cannot be used to compute the provenance in an application semiring.
It may still be interesting to consider this case for explaining entailments
with more details than with the $\sf{Why}[{\sf X}]$-provenance. Possible
directions for future work also include considering other query answering
methods for ${\cal E\\!LHI}_{\bot}$, for example based on Datalog rewritings
(?). Finally, extension of the semiring provenance semantics to more
expressive DLs featuring disjunction and full negation remains a challenge
(cf. discussion in Section 6).

## Acknowledgements

This work was supported by the ANR project CQFD (ANR-18-CE23-0003), by the MUR
for the Department of Excellence DISCo at the University of Milano-Bicocca and
under the PRIN project PINPOINT Prot. 2020FNEB27, CUP H45E21000210001. Ozaki
is supported by the NFR project “Learning Description Logic Ontologies,” grant
number 316022.

##  A Proofs for Section 3

See 3.6

###### Proof.

Claim (i): Let $\mathcal{I}$ be a model of $\mathcal{O}$ and define
$\mathcal{I}^{\mathbb{K}}_{0}=(\Delta^{\mathcal{I}},K,\cdot^{\mathcal{I}^{\mathbb{K}}_{0}})$
as follows:

  * •

$a^{\mathcal{I}^{\mathbb{K}}_{0}}=a^{\mathcal{I}}$ for every $a\in{\sf
N_{I}}$,

  * •

$A^{\mathcal{I}^{\mathbb{K}}_{0}}=\\{(d,\mathbb{0})\mid d\in
A^{\mathcal{I}}\\}\cup\\{(a^{\mathcal{I}},\kappa)\mid(A(a),\kappa)\in\mathcal{O}^{\mathbb{K}}\\}$
for every $A\in{\sf N_{C}}$,

  * •

$R^{\mathcal{I}^{\mathbb{K}}_{0}}=\\{(d,e,\mathbb{0})\mid(d,e)\in
R^{\mathcal{I}}\\}\cup\\{(a^{\mathcal{I}},b^{\mathcal{I}},\kappa)\mid(R(a,b),\kappa)\in\mathcal{O}^{\mathbb{K}}\\}$
for every $R\in{\sf N_{R}}$.

Then given $\mathcal{I}^{\mathbb{K}}_{n}$, we define
$\mathcal{I}^{\mathbb{K}}_{n+1}$ by applying one of the following rules:

$\begin{array}[]{l}\text{(1) if }({P\sqsubseteq
Q},{\kappa})\in\mathcal{O}^{\mathbb{K}},(d,e,\kappa^{\prime})\in
P^{\mathcal{I}^{\mathbb{K}}_{n}}\text{ then
}(d,e,\kappa\otimes\kappa^{\prime})\in
Q^{\mathcal{I}^{\mathbb{K}}_{n+1}}\\!;\\\ \text{(2) if }({C\sqsubseteq
A},{\kappa})\in\mathcal{O}^{\mathbb{K}},(d,\kappa^{\prime})\in
C^{\mathcal{I}^{\mathbb{K}}_{n}}\text{ then
}(d,\kappa\otimes\kappa^{\prime})\in A^{\mathcal{I}^{\mathbb{K}}_{n+1}}\\!;\\\
\text{(3) if }({C\sqsubseteq\exists
P},{\kappa})\in\mathcal{O}^{\mathbb{K}},(d,\kappa^{\prime})\in
C^{\mathcal{I}^{\mathbb{K}}_{n}}\text{ and }(d,e)\in P^{\mathcal{I}}\text{
then }(d,e,\kappa\otimes\kappa^{\prime})\in
P^{\mathcal{I}^{\mathbb{K}}_{n+1}}.\\\ \end{array}$

and let $\mathcal{I}^{\mathbb{K}}:=\bigcup_{n\geq
0}\mathcal{I}^{\mathbb{K}}_{n}$.

We show by induction that for every $n$, $\mathcal{I}$ and
$\mathcal{I}^{\mathbb{K}}_{n}$ coincide on their non-annotated part. First
note that if $\mathcal{I}$ and $\mathcal{I}^{\mathbb{K}}_{n}$ coincide on
their non-annotated part, for every ${\cal E\\!LHI}_{\bot}$ concept $C$,
$C^{\mathcal{I}}=\\{d\mid(d,\kappa)\in C^{\mathcal{I}^{\mathbb{K}}_{n}}\\}$
(this can be shown very easily by structural induction).

  * •

Base case: $\mathcal{I}$ and $\mathcal{I}^{\mathbb{K}}_{0}$ coincide on their
non-annotated part by definition of $\mathcal{I}^{\mathbb{K}}_{0}$ and the
fact that annotated assertions of $\mathcal{O}^{\mathbb{K}}$ have their non-
annotated counterpart in $\mathcal{O}$.

  * •

Induction step. If $\mathcal{I}^{\mathbb{K}}_{n+1}$ is obtained from
$\mathcal{I}^{\mathbb{K}}_{n}$ by applying rule (1), $(P\sqsubseteq
Q,\kappa)\in\mathcal{O}^{\mathbb{K}}$ and $(d,e,\kappa^{\prime})\in
P^{\mathcal{I}^{\mathbb{K}}_{n}}$. By induction hypothesis $(d,e)\in
P^{\mathcal{I}}$ so since $\mathcal{I}\models P\sqsubseteq Q$, $(d,e)\in
Q^{\mathcal{I}}$ and $\mathcal{I}^{\mathbb{K}}_{n+1}$ and $\mathcal{I}$
coincide on their non-annotated part. If $\mathcal{I}^{\mathbb{K}}_{n+1}$ is
obtained from $\mathcal{I}^{\mathbb{K}}_{n}$ by applying rule (2),
$(C\sqsubseteq A,\kappa)\in\mathcal{O}^{\mathbb{K}}$ and
$(d,\kappa^{\prime})\in C^{\mathcal{I}^{\mathbb{K}}_{n}}$. By induction
hypothesis $d\in C^{\mathcal{I}}$ so since $\mathcal{I}\models C\sqsubseteq
A$, $d\in A^{\mathcal{I}}$ and $\mathcal{I}^{\mathbb{K}}_{n+1}$ and
$\mathcal{I}$ coincide on their non-annotated part. The case where
$\mathcal{I}^{\mathbb{K}}_{n+1}$ is obtained from
$\mathcal{I}^{\mathbb{K}}_{n}$ by applying rule (3) is straightforward since
rule (3) requires $(d,e)\in P^{\mathcal{I}}$.

We now show that $\mathcal{I}^{\mathbb{K}}$ is a model of
$\mathcal{O}^{\mathbb{K}}$.

  * •

For every annotated concept assertion
$(A(a),\kappa)\in\mathcal{O}^{\mathbb{K}}$, $(a^{\mathcal{I}},\kappa)\in
A^{\mathcal{I}^{\mathbb{K}}_{0}}$ so
$\mathcal{I}^{\mathbb{K}}\models(A(a),\kappa)$, and similarly for role
assertions.

  * •

Let $(P\sqsubseteq Q,\kappa)$ be an annotated RI in
$\mathcal{O}^{\mathbb{K}}$. Rule (1) ensures that
$\mathcal{I}^{\mathbb{K}}\models(P\sqsubseteq Q,\kappa)$.

  * •

Let $(P\sqcap Q\sqsubseteq\bot,\kappa)$ be an annotated negative RI in
$\mathcal{O}^{\mathbb{K}}$. There cannot exist $(d,e,\kappa_{1})\in
P^{\mathcal{I}^{\mathbb{K}}}$ and $(d,e,\kappa_{2})\in
Q^{\mathcal{I}^{\mathbb{K}}}$ since this would contradict the fact that
$\mathcal{I}$ and $\mathcal{I}^{\mathbb{K}}$ coincide on their non-annotated
part and $\mathcal{I}$ is a model of $\mathcal{O}$. Thus
$\mathcal{I}^{\mathbb{K}}\models(P\sqcap Q\sqsubseteq\bot,\kappa)$.

  * •

Let $(C\sqsubseteq D,\kappa)$ be an annotated GCI in
$\mathcal{O}^{\mathbb{K}}$. If $D=\bot$, then
$C^{\mathcal{I}^{\mathbb{K}}}=\emptyset$ (otherwise this would contradict the
fact that $\mathcal{I}$ and $\mathcal{I}^{\mathbb{K}}$ coincide on their non-
annotated part and $\mathcal{I}$ is a model of $\mathcal{O}$). If $D\in{\sf
N_{C}}$, rule (2) ensures that $\mathcal{I}^{\mathbb{K}}\models(C\sqsubseteq
D,\kappa)$. Finally, if $D=\exists P$, let $(d,\kappa^{\prime})\in
C^{\mathcal{I}^{\mathbb{K}}}$. Since $\mathcal{I}$ and
$\mathcal{I}^{\mathbb{K}}$ coincide on their non-annotated part, $d\in
C^{\mathcal{I}}$, and since $\mathcal{I}\models C\sqsubseteq D$, there exists
$(d,e)\in P^{\mathcal{I}}$. Hence, by rule (3),
$(d,e,\kappa\otimes\kappa^{\prime})\in P^{\mathbb{K}}$, i.e.
$(d,\kappa\otimes\kappa^{\prime})\in D^{\mathcal{I}^{\mathbb{K}}}$. Hence
$\mathcal{I}^{\mathbb{K}}\models(C\sqsubseteq D,\kappa)$.

Claim (ii): It follows straightforwardly from the definitions of models and
annotated models that the interpretation obtained from a model
$\mathcal{I}^{\mathbb{K}}$ of $\mathcal{O}^{\mathbb{K}}$ by dropping the
annotations is a model of $\mathcal{O}$. ∎

See 3.9

###### Proof.

The proof is made by structural induction. In the base case, $C\in{\sf
N_{C}}\cup\\{\top\\}$ and $\boldsymbol{q_{C}}(x)=\exists t_{0}\,C(x,t_{0})$:

$\displaystyle\\{\bigotimes_{P(\vec{t},t)\in\boldsymbol{q_{C}}(x)}\pi(t)\mid\pi\in\nu_{\mathcal{I}}(\boldsymbol{q_{C}}(x)),\pi(x)=d\\}=\\{\pi(t_{0})\mid\pi\in\nu_{\mathcal{I}}(C(d,t_{0}))\\}=\\{\kappa\mid(d,\kappa)\in
C^{\mathcal{I}}\\}.$

Induction step. If $C=C_{1}\sqcap C_{2}$, then
$\boldsymbol{q_{C}}(x)=\boldsymbol{q_{1}}(x)\wedge\boldsymbol{q_{2}}(x)$ where
$\boldsymbol{q_{1}}(x)$ and $\boldsymbol{q_{2}}(x)$ are the extended versions
of the queries that retrieve the instances of $C_{1}$ and $C_{2}$
respectively.

$\displaystyle\\{\bigotimes_{P(\vec{t},t)\in\boldsymbol{q_{C}}(x)}\pi(t)\mid\pi\in\nu_{\mathcal{I}}(\boldsymbol{q_{C}}(x)),\pi(x)=d\\}=$
$\displaystyle\\{\bigotimes_{P(\vec{t},t)\in\boldsymbol{q_{1}}(x)}\pi_{1}(t)\otimes\bigotimes_{P(\vec{t},t)\in\boldsymbol{q_{2}}(x)}\pi_{2}(t)\mid$
$\displaystyle\pi_{1}\in\nu_{\mathcal{I}}(\boldsymbol{q_{1}}$
$\displaystyle(x)),\pi_{2}\in\nu_{\mathcal{I}}(\boldsymbol{q_{2}}(x)),\pi_{1}(x)=\pi_{2}(x)=d\\}$
$\displaystyle=$
$\displaystyle\\{\kappa_{1}\otimes\kappa_{2}\mid(d,\kappa_{1})\in
C_{1}^{\mathcal{I}},(d,\kappa_{2})\in C_{2}^{\mathcal{I}}\\}$ $\displaystyle=$
$\displaystyle\\{\kappa\mid(d,\kappa)\in C^{\mathcal{I}}\\}$

If $C=\exists R.C_{1}$, then $\boldsymbol{q_{C}}(x)=\exists
yt_{0}\,R(x,y,t_{0})\wedge\boldsymbol{q_{1}}(y)$ where $\boldsymbol{q_{1}}(y)$
is the extended version of the query that retrieves the instances of $C_{1}$.

$\displaystyle\\{\bigotimes_{P(\vec{t},t)\in\boldsymbol{q_{C}}(x)}\pi(t)\mid\pi\in\nu_{\mathcal{I}}(\boldsymbol{q_{C}}(x)),\pi(x)=d\\}=$
$\displaystyle\\{\pi_{R}(t_{0})\otimes\bigotimes_{P(\vec{t},t)\in\boldsymbol{q_{1}}(x)}\pi_{1}(t)\mid$
$\displaystyle\pi_{R}\in\nu_{\mathcal{I}}(R(x,y,t_{0})),$
$\displaystyle\pi_{1}\in\nu_{\mathcal{I}}(\boldsymbol{q_{1}}(y)),\pi_{R}(x)=d,\pi_{1}(y)=\pi_{R}(y)\\}$
$\displaystyle=$
$\displaystyle\\{\kappa_{R}\otimes\kappa_{1}\mid(d,e,\kappa_{R})\in
R^{\mathcal{I}},(e,\kappa_{1})\in C_{1}^{\mathcal{I}}\\}$ $\displaystyle=$
$\displaystyle\\{\kappa\mid(d,\kappa)\in C^{\mathcal{I}}\\}$

The case $C=\exists R^{-}.C_{1}$, where $\boldsymbol{q_{C}}(x)=\exists
yt_{0}\,R(y,x,t_{0})\wedge\boldsymbol{q_{1}}(y)$, is similar.∎

See 3.10

###### Proof.

By Lemma 3.9, for every model $\mathcal{I}$ of $\mathcal{O}^{\mathbb{K}}$,
${\sf
prov}_{\mathcal{I}}({\boldsymbol{q_{C}}(a)})=\\{\bigotimes_{P(\vec{t},t)\in\boldsymbol{q_{C}}(a)}\pi(t)\mid\pi\in\nu_{\mathcal{I}}(\boldsymbol{q_{C}}(a))\\}=\\{\kappa\mid(a^{\mathcal{I}},\kappa)\in
C^{\mathcal{I}}\\}.$

Moreover, (i) for every model $\mathcal{I}$ of
$\mathcal{O}^{\mathbb{K}}\cup\\{(C\sqsubseteq A_{C},\mathbb{1})\\}$,
$C^{\mathcal{I}}\subseteq A_{C}^{\mathcal{I}}$ and the annotated
interpretation $\mathcal{J}$ obtained from $\mathcal{I}$ by setting
$A_{C}^{\mathcal{J}}=C^{\mathcal{I}}$ is also a model of
$\mathcal{O}^{\mathbb{K}}\cup\\{(C\sqsubseteq A_{C},\mathbb{1})\\}$, so
$\bigcap_{\mathcal{I}\models\mathcal{O}^{\mathbb{K}}\cup\\{(C\sqsubseteq
A_{C},\mathbb{1})\\}}\\{\chi\mid(a^{\mathcal{I}},\chi)\in
A_{C}^{\mathcal{I}}\\}=\bigcap_{\mathcal{I}\models\mathcal{O}^{\mathbb{K}}\cup\\{(C\sqsubseteq
A_{C},\mathbb{1})\\}}\\{\chi\mid(a^{\mathcal{I}},\chi)\in C^{\mathcal{I}}\\}$,
and (ii) models of $\mathcal{O}^{\mathbb{K}}\cup\\{(C\sqsubseteq
A_{C},\mathbb{1})\\}$ are models of $\mathcal{O}^{\mathbb{K}}$ and for every
model $\mathcal{I}$ of $\mathcal{O}^{\mathbb{K}}$, the interpretation
$\mathcal{J}$ that extends $\mathcal{I}$ by setting
$A_{C}^{\mathcal{J}}=C^{\mathcal{I}}$ is a model of
$\mathcal{O}^{\mathbb{K}}\cup\\{(C\sqsubseteq A_{C},\mathbb{1})\\}$ so
$\bigcap_{\mathcal{I}\models\mathcal{O}^{\mathbb{K}}}\\{\chi\mid(a^{\mathcal{I}},\chi)\in
C^{\mathcal{I}}\\}=\bigcap_{\mathcal{I}\models\mathcal{O}^{\mathbb{K}}\cup\\{(C\sqsubseteq
A_{C},\mathbb{1})\\}}\\{\chi\mid(a^{\mathcal{I}},\chi)\in C^{\mathcal{I}}\\}$.
It follows that

$\displaystyle\mathcal{P}(A_{C}(a),\mathcal{O}^{\mathbb{K}}\cup\\{(C\sqsubseteq
A_{C},\mathbb{1})\\})=$
$\displaystyle\bigoplus_{\mathcal{O}^{\mathbb{K}}\cup\\{(C\sqsubseteq
A_{C},\mathbb{1})\\}\models(A_{C}(a),\kappa)}\kappa$ $\displaystyle=$
$\displaystyle\bigoplus_{\kappa\in\bigcap_{\mathcal{I}\models\mathcal{O}^{\mathbb{K}}\cup\\{(C\sqsubseteq
A_{C},\mathbb{1})\\}}\\{\chi\mid(a^{\mathcal{I}},\chi)\in
A_{C}^{\mathcal{I}}\\}}\kappa$ $\displaystyle=$
$\displaystyle\bigoplus_{\kappa\in\bigcap_{\mathcal{I}\models\mathcal{O}^{\mathbb{K}}\cup\\{(C\sqsubseteq
A_{C},\mathbb{1})\\}}\\{\chi\mid(a^{\mathcal{I}},\chi)\in
C^{\mathcal{I}}\\}}\kappa$ $\displaystyle=$
$\displaystyle\bigoplus_{\kappa\in\bigcap_{\mathcal{I}\models\mathcal{O}^{\mathbb{K}}}\\{\chi\mid(a^{\mathcal{I}},\chi)\in
C^{\mathcal{I}}\\}}\kappa$ $\displaystyle=$
$\displaystyle\bigoplus_{\kappa\in\bigcap_{\mathcal{I}\models\mathcal{O}^{\mathbb{K}}}{\sf
prov}_{\mathcal{I}}({\boldsymbol{q_{C}}(a)})}\kappa$ $\displaystyle=$
$\displaystyle\ \mathcal{P}(q_{C}(a),\mathcal{O}^{\mathbb{K}}).\qed$

###  A.1 Relationship with Semantics for Specific Annotations

The proof of Proposition 3.11 uses the canonical model of an annotated
ontology introduced in Section 3.4. This is not an issue because Proposition
3.11 is not use to prove any result related to the canonical model.

See 3.11

###### Proof.

($\Leftarrow$) Consider a satisfiable annotated ${\cal E\\!LHI}_{\bot}$
ontology $\mathcal{O}^{\mathbb{F}}$. For any given annotated interpretation
$\mathcal{I}=(\Delta^{\mathcal{I}},[0,1],\cdot^{\mathcal{I}})$ and
$n\in[0,1]$, we construct the classical interpretation $\mathcal{I}_{\geq
n}=(\Delta^{\mathcal{I}},\cdot^{\mathcal{I}_{\geq n}})$ where

  * •

for each $a\in{\sf N_{I}}$, $a^{\mathcal{I}_{\geq n}}=a^{\mathcal{I}}$;

  * •

for each $A\in{\sf N_{C}}$, $A^{\mathcal{I}_{\geq
n}}=\\{d\mid\exists\kappa\geq n\text{ s.t. }(d,\kappa)\in A^{\mathcal{I}}\\}$;
and

  * •

for each $R\in{\sf N_{R}}$, $R^{\mathcal{I}_{\geq
n}}=\\{(d,e)\mid\exists\kappa\geq n\text{ s.t. }(d,e,\kappa)\in
R^{\mathcal{I}}\\}$.

One can show by structural induction that for every concept $C$ and every role
$S$, it holds that $C^{\mathcal{I}_{\geq n}}=\\{d\mid\exists\kappa\geq n\text{
s.t. }(d,\kappa)\in C^{\mathcal{I}}\\}$ and $S^{\mathcal{I}_{\geq
n}}=\\{(d,e)\mid\exists\kappa\geq n\text{ s.t. }(d,e,\kappa)\in
S^{\mathcal{I}}\\}$. Using this property, we show that if $\mathcal{I}$ is a
model of $\mathcal{O}^{\mathbb{F}}$ then $\mathcal{I}_{\geq n}$ is a model of
$\mathcal{O}_{\geq n}$.

  * •

If $A(a)\in\mathcal{O}_{\geq n}$ then
$(A(a),\kappa)\in\mathcal{O}^{\mathbb{F}}$, for some $\kappa\geq n$. Since
$\mathcal{I}\models\mathcal{O}^{\mathbb{F}}$, it follows that
$(a^{\mathcal{I}},\kappa)\in A^{\mathcal{I}}$ and by construction
$a^{\mathcal{I}}\in A^{\mathcal{I}_{\geq n}}$, which implies
$\mathcal{I}_{\geq n}\models A(a)$. The case for role assertions follows
analogously.

  * •

If $C\sqsubseteq D\in\mathcal{O}_{\geq n}$ then $(C\sqsubseteq
D,\kappa)\in\mathcal{O}^{\mathbb{F}}$, for some $\kappa\geq n$. Consider some
$d\in C^{\mathcal{I}_{\geq n}}$. By the property above, there exists
$\kappa^{\prime}\geq n$ such that $(d,\kappa^{\prime})\in C^{\mathcal{I}}$.
Since $\mathcal{I}\models\mathcal{O}^{\mathbb{F}}$ it follows that
$(d,\min(\kappa,\kappa^{\prime}))\in D^{\mathcal{I}}$ (recall that $\min$ is
the semiring product in the fuzzy semiring). But then this means that $d\in
D^{\mathcal{I}_{\geq n}}$ as both $\kappa$ and $\kappa^{\prime}$ are greater
or equal to $n$. As $d$ was an arbitrary element, we get that
$\mathcal{I}_{\geq n}\models C\sqsubseteq D$. The case for role inclusions can
be treated analogously.

Point (1): Let $\alpha$ be a BCQ (or an assertion) and suppose that
$\mathcal{P}(\alpha,\mathcal{O}^{\mathbb{F}})<n$. By Theorem 3.14, since
$\mathcal{O}^{\mathbb{F}}$ is satisfiable, its canonical model
$\mathcal{I}_{\mathcal{O}^{\mathbb{F}}}$ is such that
$\mathcal{O}^{\mathbb{F}}\models(\alpha,\kappa)$ iff
$\mathcal{I}_{\mathcal{O}^{\mathbb{F}}}\models(\alpha,\kappa)$. Hence, since
$\mathcal{P}(\alpha,\mathcal{O}^{\mathbb{F}})=\max_{\mathcal{O}^{\mathbb{F}}\models(\alpha,\kappa)}(\kappa)$,
it holds that
$\mathcal{I}_{\mathcal{O}^{\mathbb{F}}}\not\models(\alpha,\kappa)$ for every
$\kappa\geq n$. Let $\mathcal{I}_{\geq n}$ be defined as explained above for
$\mathcal{I}=\mathcal{I}_{\mathcal{O}^{\mathbb{F}}}$. Since
$\mathcal{I}_{\mathcal{O}^{\mathbb{F}}}$ is a model of
$\mathcal{O}^{\mathbb{F}}$, $\mathcal{I}_{\geq n}$ is a model of
$\mathcal{O}_{\geq n}$. We show that $\mathcal{I}_{\geq n}\not\models\alpha$.
Since $\mathcal{I}_{\mathcal{O}^{\mathbb{F}}}\not\models(\alpha,\kappa)$ for
every $\kappa\geq n$, there is no match for $\alpha$ in
$\mathcal{I}_{\mathcal{O}^{\mathbb{F}}}$ such that all annotations are greater
or equal to $n$. Hence $\mathcal{I}_{\geq n}\not\models\alpha$. It follows
that $\mathcal{O}_{\geq n}\not\models\alpha$.

Point (2): Assume that $\mathcal{O}$ does not feature $\bot$ and let $\alpha$
be a GCI between basic concepts $C\sqsubseteq D$. Since $\mathcal{O}$ does not
feature $\bot$, $C$ and $D$ are satisfiable w.r.t. $\mathcal{O}^{\mathbb{F}}$.
By Theorem 3.17, since $\mathbb{F}$ is $\otimes$-idempotent, it holds that
$(d_{C},\kappa)\in D^{\mathcal{I}_{C,\mathcal{O}^{\mathbb{F}}}}$ iff
${\mathcal{O}^{\mathbb{F}}}\models(C\sqsubseteq D,\kappa)$ where
$\mathcal{I}_{C,\mathcal{O}^{\mathbb{F}}}$ is the canonical model for $C$ and
$\mathcal{O}^{\mathbb{F}}$. Hence, since
$\mathcal{P}(\alpha,\mathcal{O}^{\mathbb{F}})=\max_{\mathcal{O}^{\mathbb{F}}\models(\alpha,\kappa)}(\kappa)$,
it holds that $(d_{C},\kappa)\notin
D^{\mathcal{I}_{C,\mathcal{O}^{\mathbb{F}}}}$ for every $\kappa\geq n$. Let
$\mathcal{I}_{\geq n}$ be defined as explained above for
$\mathcal{I}=\mathcal{I}_{C,\mathcal{O}^{\mathbb{F}}}$. Since
$\mathcal{I}_{C,\mathcal{O}^{\mathbb{F}}}$ is a model of
$\mathcal{O}^{\mathbb{F}}$, $\mathcal{I}_{\geq n}$ is a model of
$\mathcal{O}_{\geq n}$. We show that $\mathcal{I}_{\geq n}\not\models\alpha$.
Since $(d_{C},1)\in C^{\mathcal{I}_{C,\mathcal{O}^{\mathbb{F}}}}$ by
construction of $\mathcal{I}_{C,\mathcal{O}^{\mathbb{F}}}$, then $d_{C}\in
C^{\mathcal{I}_{\geq n}}$, and since $(d_{C},\kappa)\notin
D^{\mathcal{I}_{C,\mathcal{O}^{\mathbb{F}}}}$ for every $\kappa\geq n$, then
$d_{C}\notin D^{\mathcal{I}_{\geq n}}$. It follows that $\mathcal{I}_{\geq
n}\not\models\alpha$. Hence $\mathcal{O}_{\geq n}\not\models\alpha$.

($\Rightarrow$) Let
$\textsf{val}(\mathcal{O}^{\mathbb{F}}):=\\{\kappa\mid\exists\alpha\text{ s.t.
}(\alpha,\kappa)\in\mathcal{O}^{\mathbb{F}}\\}\cup\\{1\\}$ be the set of all
annotations appearing in $\mathcal{O}^{\mathbb{F}}$. Given a classical
interpretation $\mathcal{I}=(\Delta^{\mathcal{I}},\cdot^{\mathcal{I}})$ we
construct the annotated interpretation
$\mathcal{I}_{\mathbb{F}}=(\Delta^{\mathcal{I}},[0,1],\cdot^{\mathcal{I}_{\mathbb{F}}})$
where

  * •

for each $a\in{\sf N_{I}}$, $a^{\mathcal{I}_{\mathbb{F}}}=a^{\mathcal{I}}$;

  * •

for each $A\in{\sf N_{C}}$,

$A^{\mathcal{I}_{\mathbb{F}}}=\\{(d,\kappa)\mid d\in
A^{\mathcal{I}},\kappa\in\textsf{val}(\mathcal{O}^{\mathbb{F}})\\}\cup\\{(d,\kappa)\mid
d\in\Delta^{\mathcal{I}}\setminus
A^{\mathcal{I}},\kappa\in\textsf{val}(\mathcal{O}^{\mathbb{F}})\cap[0,n)\\};$

  * •

for each $R\in{\sf N_{R}}$,

$R^{\mathcal{I}_{\mathbb{F}}}=\\{(d,e,\kappa)\mid(d,e)\in
R^{\mathcal{I}},\kappa\in\textsf{val}(\mathcal{O}^{\mathbb{F}})\\}\cup\\{(d,e,\kappa)\mid(d,e)\notin
R^{\mathcal{I}},\kappa\in\textsf{val}(\mathcal{O}^{\mathbb{F}})\cap[0,n)\\}.$

It is a simple induction exercise to see that the properties given by these
definitions extend to arbitrary concepts and roles. In words,
$\mathcal{I}_{\mathbb{F}}$ associates all values in
$\textsf{val}(\mathcal{O}^{\mathbb{F}})$ to every property satisfied by
$\mathcal{I}$, and only those values smaller than $n$ to the properties not
satisfied by $\mathcal{I}$. Let $\mathcal{O}^{\prime}$ be the ontology
obtained from $\mathcal{O}$ by removing all GCIs or RIs that have $\bot$ in
their right-hand side. We show that if $\mathcal{I}\models\mathcal{O}_{\geq
n}$, then
$\mathcal{I}_{\mathbb{F}}\models\mathcal{O}^{{}^{\prime}\mathbb{F}}$.

  * •

For $(A(a),\kappa)\in\mathcal{O}^{\mathbb{F}}$, if $\kappa<n$ then by
construction $(a^{\mathcal{I}},\kappa)\in A^{\mathcal{I}_{\mathbb{F}}}$; if
$\kappa\geq n$, then $A(a)\in\mathcal{O}_{\geq n}$ and since $\mathcal{I}$ is
a model of $\mathcal{O}_{\geq n}$, $a^{\mathcal{I}}\in A^{\mathcal{I}}$ which
implies that $(a^{\mathcal{I}},\kappa)\in A^{\mathcal{I}_{\mathbb{F}}}$. Role
assertions hold analogously.

  * •

Given $(C\sqsubseteq D,\kappa)\in\mathcal{O}^{\mathbb{F}}$ with $D\neq\bot$
and $(d,\kappa^{\prime})\in C^{\mathcal{I}_{\mathbb{F}}}$, if
$\kappa^{\prime}<n$ or $\kappa<n$, then $\min(\kappa^{\prime},\kappa)<n$ and
hence $(d,\min(\kappa^{\prime},\kappa))\in D^{\mathcal{I}_{\mathbb{F}}}$; if
$\min(\kappa^{\prime},\kappa)\geq n$, then we know that $d\in C^{\mathcal{I}}$
and $C\sqsubseteq D\in\mathcal{O}_{\geq n}$. Since $\mathcal{I}$ is a model of
$\mathcal{O}_{\geq n}$, we get $d\in D^{\mathcal{I}}$ which implies that
$(d,\min(\kappa^{\prime},\kappa))\in D^{\mathcal{I}_{\mathbb{F}}}$. Positive
role inclusions hold analogously.

Let $\alpha$ be a BCQ or a GCI and assume that $\mathcal{O}_{\geq
n}\not\models\alpha$. There is a model $\mathcal{I}$ of $\mathcal{O}_{\geq n}$
such that $\mathcal{I}\not\models\alpha$. We show that
$\mathcal{I}_{\mathbb{F}}\not\models(\alpha,\kappa)$ for all $\kappa\geq n$.
Let $\kappa\geq n$.

  * •

If $\alpha$ is a GCI of the form $C\sqsubseteq D$,
$\mathcal{I}\not\models\alpha$ means that there must exist a $d\in
C^{\mathcal{I}}$ such that $d\notin D^{\mathcal{I}}$. By construction of
$\mathcal{I}_{\mathbb{F}}$, it follows that $(d,1)\in
C^{\mathcal{I}_{\mathbb{F}}}$ but then $(d,\min(1,\kappa))=(d,\kappa)\notin
D^{\mathcal{I}_{\mathbb{F}}}$ since $\kappa\geq n$. Hence
$\mathcal{I}_{\mathbb{F}}\not\models(C\sqsubseteq D,\kappa)$.

  * •

If $\alpha$ be a BCQ (or assertion), $\mathcal{I}\not\models\alpha$ means that
there is no match for $\alpha$ in $\mathcal{I}$, hence no match for $\alpha$
in the part of $\mathcal{I}_{\mathbb{F}}$ annotated with elements greater or
equal to $n$. Hence $\mathcal{I}_{\mathbb{F}}\not\models(\alpha,\kappa)$ for
all $\kappa\geq n$.

It follows that
$\mathcal{O}^{{}^{\prime}\mathbb{F}}\not\models(\alpha,\kappa)$ for all
$\kappa\geq n$.

Point (1): Assume that $\alpha$ is a BCQ. By Theorem 3.14, since
$\mathcal{O}^{\mathbb{F}}$ is satisfiable, its canonical model
$\mathcal{I}_{\mathcal{O}^{\mathbb{F}}}$ is such that
$\mathcal{O}^{\mathbb{F}}\models(\alpha,\kappa)$ iff
$\mathcal{I}_{\mathcal{O}^{\mathbb{F}}}\models(\alpha,\kappa)$. The same holds
for ${\mathcal{O}^{\prime}}^{\mathbb{F}}$ which is trivially satisfiable.
Moreover, the construction of the canonical model does not depend on the
negative GCIs or RIs of the ontology, hence $\mathcal{O}^{\mathbb{F}}$ and
${\mathcal{O}^{\prime}}^{\mathbb{F}}$ have the same canonical model. It
follows that $\mathcal{O}^{\mathbb{F}}\not\models(\alpha,\kappa)$ for all
$\kappa\geq n$, thus $\mathcal{P}(\alpha,\mathcal{O}^{\mathbb{F}})<n$.

Point (2): If $\mathcal{O}$ does not feature $\bot$, it holds that
$\mathcal{O}^{\prime}=\mathcal{O}$. Hence we obtain that
$\mathcal{O}^{\mathbb{F}}\not\models(\alpha,\kappa)$ for all $\kappa\geq n$,
thus $\mathcal{P}(\alpha,\mathcal{O}^{\mathbb{F}})<n$. ∎

###  A.2 Canonical Model

######  Lemma A.1.

Let $\mathcal{I}=(\Delta^{\mathcal{I}},K,\cdot^{\mathcal{I}})$ and
$\mathcal{J}=(\Delta^{\mathcal{J}},K,\cdot^{\mathcal{J}})$ be
$\mathbb{K}$-annotated interpretations such that there is a homomorphism
$g:\mathcal{I}\rightarrow\mathcal{J}$. For every $\kappa\in K$ and every
${\cal E\\!LHI}_{\bot}$ concept expression $C$, if $(d,\kappa)\in
C^{\mathcal{I}}$ then $(g(d),\kappa)\in C^{\mathcal{J}}$.

###### Proof.

The proof is by structural induction. In the base case, $C$ is a concept name
$A$ and the lemma holds by definition of $g$. For $C=\top$ the lemma holds
trivially. Now, suppose that the lemma holds for $D,D_{1},D_{2}$. We make a
case distinction:

  * •

$C=D_{1}\sqcap D_{2}$: if $(d,\kappa)\in(D_{1}\sqcap D_{2})^{\mathcal{I}}$
then, by the semantics of $\mathbb{K}$-annotated ${\cal E\\!LHI}_{\bot}$,
there exist $(d,\kappa_{1})\in D^{\mathcal{I}}_{1}$ and $(d,\kappa_{2})\in
D^{\mathcal{I}}_{2}$ such that $\kappa=\kappa_{1}\otimes\kappa_{2}$. By the
inductive hypothesis, $(g(d),\kappa_{1})\in D^{\mathcal{J}}_{1}$ and
$(g(d),\kappa_{2})\in D^{\mathcal{J}}_{2}$. Then, by the semantics of
$\mathbb{K}$-annotated ${\cal E\\!LHI}_{\bot}$, we have that
$(g(d),\kappa)\in(D_{1}\sqcap D_{2})^{\mathcal{J}}$.

  * •

$C=\exists P.D$ (where $P$ can be a role name or an inverse role): if
$(d,\kappa)\in(\exists P.D)^{\mathcal{I}}$ then, by the semantics of
$\mathbb{K}$-annotated ${\cal E\\!LHI}_{\bot}$, there exist
$e\in\Delta^{\mathcal{I}}$ with $(d,e,\kappa_{1})\in P^{\mathcal{I}}$ and
$(e,\kappa_{2})\in D^{\mathcal{I}}$ such that
$\kappa=\kappa_{1}\otimes\kappa_{2}$. By definition of $g$, we have that
$(d,e,\kappa_{1})\in P^{\mathcal{I}}$ implies $(g(d),g(e),\kappa_{1})\in
P^{\mathcal{J}}$ and, by the inductive hypothesis, $(g(e),\kappa_{2})\in
D^{\mathcal{J}}$. Then, by the semantics of $\mathbb{K}$-annotated ${\cal
E\\!LHI}_{\bot}$, we have that $(g(d),\kappa)\in(\exists P.D)^{\mathcal{J}}$.
∎

######  Lemma A.2.

Let $\mathcal{I}=(\Delta^{\mathcal{I}},K,\cdot^{\mathcal{I}})$ and
$\mathcal{J}=(\Delta^{\mathcal{J}},K,\cdot^{\mathcal{J}})$ be
$\mathbb{K}$-annotated interpretations such that there is a homomorphism
$g:\mathcal{I}\rightarrow\mathcal{J}$. For every $\kappa\in K$ and every BCQ
$q$, if $\mathcal{I}\models(q,\kappa)$ then $\mathcal{J}\models(q,\kappa)$.

###### Proof.

Assume $\mathcal{I}\models(q,\kappa)$ and let $\boldsymbol{q}$ be the extended
version of $q$. Denote by $\nu_{\mathcal{I}}(\boldsymbol{q})$ the set of all
matches of $\boldsymbol{q}$ in $\mathcal{I}$. By semantics of $(q,\kappa)$, we
have that $\mathcal{I}\models(q,\kappa)$ iff there is a match
$\pi:\mathsf{terms}(\boldsymbol{q})\rightarrow\Delta^{\mathcal{I}}\cup K$ in
$\nu_{\mathcal{I}}(\boldsymbol{q})$ such that
$\kappa=\bigotimes_{P(\vec{t},t)\in\boldsymbol{q}}\pi(t)$. To prove this
lemma, we need to construct a match
$\pi^{\prime}:\mathsf{terms}(\boldsymbol{q})\rightarrow\Delta^{\mathcal{J}}\cup
K$ such that
$\kappa=\bigotimes_{P(\vec{t},t)\in\boldsymbol{q}}\pi^{\prime}(t)$.

For every $t\in\mathsf{terms}(\boldsymbol{q})$, we define
$\pi^{\prime}(t):=g(\pi(t))$ if $\pi(t)\notin K$ and $\pi^{\prime}(t):=\pi(t)$
otherwise. It is clear that
$\kappa=\bigotimes_{P(\vec{t},t)\in\boldsymbol{q}}\pi^{\prime}(t)$ from the
definition of $\pi^{\prime}$. We argue that $\pi^{\prime}$ is a match of
$\boldsymbol{q}$ in $\mathcal{J}$. For every $a\in{\sf N_{I}}$,
$\pi(a)=a^{\mathcal{I}}$ because $\pi$ is a match, and
$g(a^{\mathcal{I}})=a^{\mathcal{J}}$ because $g$ is a homomorphism. Hence
$\pi^{\prime}(a)=g(\pi(a))=a^{\mathcal{J}}$ for every $a\in{\sf N_{I}}$.

It remains to show that $\pi^{\prime}(\vec{t},t)\in P^{\mathcal{J}}$ for every
$P(\vec{t},t)\in\mathsf{atoms}(\boldsymbol{q})$. That is, (i)
$(\pi^{\prime}(t_{1}),\pi^{\prime}(t))\in A^{\mathcal{J}}$ for every
$A(t_{1},t)\in\mathsf{atoms}(\boldsymbol{q})$ and (ii)
$(\pi^{\prime}(t_{1}),\pi^{\prime}(t_{2}),\pi^{\prime}(t))\in R^{\mathcal{J}}$
for every $R(t_{1},t_{2},t)\in\mathsf{atoms}(\boldsymbol{q})$. (i) If
$A(t_{1},t)\in\mathsf{atoms}(\boldsymbol{q})$ then, since $\pi$ is a match,
$(\pi(t_{1}),\pi(t))\in A^{\mathcal{I}}$, where $\pi(t)$ is necessarily equal
to some $\kappa\in K$ by definition of $\mathcal{I}$. Since
$(\pi(t_{1}),\kappa)\in A^{\mathcal{I}}$ then, by definition of $g$, we have
that $(g(\pi(t_{1})),\kappa)\in A^{\mathcal{J}}$, i.e.
$(\pi^{\prime}(t_{1}),\pi^{\prime}(t))\in A^{\mathcal{J}}$, by definition of
$\pi^{\prime}$. The proof of (ii) is similar. ∎

See 3.13

###### Proof.

Let $\mathcal{I}$ be a model of $\mathcal{O}^{\mathbb{K}}$. The proof is by
induction on the sequence of interpretations of the canonical model
$\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}$. We define $g:=\bigcup_{n\geq
0}g_{n}$ and set
$g_{0}:\Delta^{\mathcal{I}_{0}}\rightarrow\Delta^{\mathcal{I}}$ with
$g_{0}(a)=a^{\mathcal{I}}$ for all $a\in\Delta^{\mathcal{I}_{0}}$ (recall that
$\Delta^{\mathcal{I}_{0}}={\sf N_{I}}$ and $a^{\mathcal{I}_{0}}=a$ for all
$a\in{\sf N_{I}}$). By definition of $\mathcal{I}_{0}$, $(a,\kappa)\in
A^{\mathcal{I}_{0}}$ iff $(A(a),\kappa)\in\mathcal{O}^{\mathbb{K}}$. Since
$\mathcal{I}$ is a model of $\mathcal{O}^{\mathbb{K}}$, if
$(A(a),\kappa)\in\mathcal{O}^{\mathbb{K}}$ then $(a^{\mathcal{I}},\kappa)\in
A^{\mathcal{I}}$. So $(a,\kappa)\in A^{\mathcal{I}_{0}}$ implies
$(g_{0}(a),\kappa)\in A^{\mathcal{I}}$. Similarly, if $(a,b,\kappa)\in
R^{\mathcal{I}_{0}}$ then $(R(a,b),\kappa)\in\mathcal{O}^{\mathbb{K}}$, so
$(a^{\mathcal{I}},b^{\mathcal{I}},\kappa)\in R^{\mathcal{I}}$. Then,
$(a,b,\kappa)\in R^{\mathcal{I}_{0}}$ implies $(g_{0}(a),g_{0}(b),\kappa)\in
R^{\mathcal{I}}$. Thus, $g_{0}$ is a homomorphism.

Suppose it was proven that $g_{n}:\mathcal{I}_{n}\rightarrow\mathcal{I}$ is a
homomorphism. We want to show that there is a homomorphism
$g_{n+1}:\mathcal{I}_{n+1}\rightarrow\mathcal{I}$. By definition of the
canonical model, given $\mathcal{I}_{n}$, the interpretation
$\mathcal{I}_{n+1}$ is the result of modifying $\mathcal{I}_{n}$ as follows:

$\begin{array}[]{l}\text{(1) if }({P\sqsubseteq
Q},{\kappa})\in\mathcal{O}^{\mathbb{K}},(d,e,\kappa^{\prime})\in
P^{\mathcal{I}_{n}}\text{ then }(d,e,\kappa\otimes\kappa^{\prime})\in
Q^{\mathcal{I}_{n+1}}\\!;\\\ \text{(2) if }({C\sqsubseteq
A},{\kappa})\in\mathcal{O}^{\mathbb{K}},(d,\kappa^{\prime})\in
C^{\mathcal{I}_{n}}\text{ then }(d,\kappa\otimes\kappa^{\prime})\in
A^{\mathcal{I}_{n+1}}\\!;\\\ \text{(3) if }({C\sqsubseteq\exists
P},{\kappa})\in\mathcal{O}^{\mathbb{K}},(d,\kappa^{\prime})\in
C^{\mathcal{I}_{n}}\text{ then
}\Delta^{\mathcal{I}_{n+1}}:=\Delta^{\mathcal{I}_{n}}\cup\\{d_{f}\\}\text{ and
}(d,d_{f},\kappa\otimes\kappa^{\prime})\in P^{\mathcal{I}_{n+1}}.\end{array}$

In the first two cases, we define $g_{n+1}:=g_{n}$ (that is the mapping
function remains unchanged). In the third case, $g_{n+1}$ is in the same way
as $g_{n}$ except that we need to map $d_{f}$ to an element of $\mathcal{I}$.
By assumption, $g_{n}$ is a homomorphism, which (by Lemma A.1) means that if
$(d,\kappa^{\prime})\in C^{\mathcal{I}_{n}}$ then
$(g_{n}(d),\kappa^{\prime})\in C^{\mathcal{I}}$. As $\mathcal{I}$ is a model
of $\mathcal{O}^{\mathbb{K}}$, if $({C\sqsubseteq\exists
P},{\kappa})\in\mathcal{O}^{\mathbb{K}}$ and $(g_{n}(d),\kappa^{\prime})\in
C^{\mathcal{I}}$ then there is $e\in\Delta^{\mathcal{I}}$ such that
$(g_{n}(d),e,\kappa\otimes\kappa^{\prime})\in P^{\mathcal{I}}$. We take a
fixed but arbitrary such $e$ and define $g_{n+1}$ in the same way as $g_{n}$
except that $g_{n+1}(d_{f}):=e$.

We now show that in each case
$g_{n+1}:\mathcal{I}_{n+1}\rightarrow\mathcal{I}$ is a homomorphism.

  * (1)

The difference between $\mathcal{I}_{n}$ and $\mathcal{I}_{n+1}$ is that now
we have $(d,e,\kappa\otimes\kappa^{\prime})\in Q^{\mathcal{I}_{n+1}}$. By
assumption $g_{n}$ is a homomorphism, so $(d,e,\kappa^{\prime})\in
P^{\mathcal{I}_{n}}$ implies that $(g_{n}(d),g_{n}(e),\kappa^{\prime})\in
P^{\mathcal{I}}$. Since in this case $g_{n+1}=g_{n}$, we also have that
$(g_{n+1}(d),g_{n+1}(e),\kappa^{\prime})\in P^{\mathcal{I}}$. As $\mathcal{I}$
is a model of $\mathcal{O}^{\mathbb{K}}$, if $({P\sqsubseteq
Q},{\kappa})\in\mathcal{O}^{\mathbb{K}}$ then
$(g_{n+1}(d),g_{n+1}(e),\kappa\otimes\kappa^{\prime})\in Q^{\mathcal{I}}$,
which means that $g_{n+1}:\mathcal{I}_{n+1}\rightarrow\mathcal{I}$ is a
homomorphism, as required.

  * (2)

In this case, the difference between $\mathcal{I}_{n}$ and $\mathcal{I}_{n+1}$
is that now we have $(d,\kappa\otimes\kappa^{\prime})\in
A^{\mathcal{I}_{n+1}}$. By assumption $g_{n}$ is a homomorphism, so (by Lemma
A.1) $(d,\kappa^{\prime})\in C^{\mathcal{I}_{n}}$ implies that
$(g_{n}(d),\kappa^{\prime})\in C^{\mathcal{I}}$. Since in this case
$g_{n+1}=g_{n}$, we also have that $(g_{n+1}(d),\kappa^{\prime})\in
C^{\mathcal{I}}$. As $\mathcal{I}$ is a model of $\mathcal{O}^{\mathbb{K}}$,
if $({C\sqsubseteq A},{\kappa})\in\mathcal{O}^{\mathbb{K}}$ then
$(g_{n+1}(d),\kappa\otimes\kappa^{\prime})\in A^{\mathcal{I}}$, which means
that $g_{n+1}:\mathcal{I}_{n+1}\rightarrow\mathcal{I}$ is a homomorphism, as
required.

  * (3)

Finally, here the difference between $\mathcal{I}_{n}$ and $\mathcal{I}_{n+1}$
is that $\Delta^{\mathcal{I}_{n+1}}:=\Delta^{\mathcal{I}_{n}}\cup\\{d_{f}\\}$
and $(d,d_{f},\kappa\otimes\kappa^{\prime})\in P^{\mathcal{I}_{n+1}}$, where
$d_{f}$ is a fresh element. In this case $g_{n+1}$ is the same as $g_{n}$
except for $g_{n+1}(d_{f})$, which is mapped to an element in
$e\in\Delta^{\mathcal{I}}$ such that
$(g_{n+1}(d),e,\kappa\otimes\kappa^{\prime})\in P^{\mathcal{I}}$ (recall that
$g_{n+1}(d)=g_{n}(d)$). So $(d,d_{f},\kappa\otimes\kappa^{\prime})\in
P^{\mathcal{I}_{n+1}}$ implies
$(g_{n+1}(d),g_{n+1}(d_{f}),\kappa\otimes\kappa^{\prime})\in P^{\mathcal{I}}$,
as required.

Since $\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}=\bigcup_{n\geq
0}\mathcal{I}_{n}$, there exists a homomorphism
$g:\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}\rightarrow\mathcal{I}$. ∎

See 3.14

###### Proof.

Since annotated BCQs subsume annotated assertions, the two first points are
consequences of the last one. Assume
$\mathcal{O}^{\mathbb{K}}\models(q,\kappa)$. By Proposition 3.12,
$\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}\models\mathcal{O}^{\mathbb{K}}$. So
$\mathcal{O}^{\mathbb{K}}\models(q,\kappa)$ implies
$\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}\models(q,\kappa)$. Conversely, assume
that $\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}\models(q,\kappa)$ and let
$\mathcal{I}$ be a model of $\mathcal{O}^{\mathbb{K}}$. By Lemma 3.13, there
exists a homomorphism
$g:\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}\rightarrow\mathcal{I}$. By Lemma
A.2, we thus have that $\mathcal{I}\models(q,\kappa)$. It follows that
$\mathcal{O}^{\mathbb{K}}\models(q,\kappa)$. ∎

See 3.15

###### Proof.

Similar to the case of Lemma 3.13, the proof is by induction on the sequence
of interpretations of the canonical model, which now is
$\mathcal{I}_{C,\kappa,\mathcal{O}^{\mathbb{K}}}$ with $C$ a basic concept. We
define $g:=\bigcup_{n\geq 0}g_{n}$ and set
$g_{0}:\Delta^{\mathcal{I}_{0}}\rightarrow\Delta^{\mathcal{I}}$ with
$g_{0}(d_{C})=d$ and $g_{0}(a)=a^{\mathcal{I}}$ for all $a\in{\sf N_{I}}$. By
definition of $\mathcal{I}_{0}$, we have that $(d_{C},\kappa)\in
C^{\mathcal{I}_{0}}$ and by assumption $(d,\kappa)\in C^{\mathcal{I}}$. Since
$C$ is a basic concept, it is a concept name $A$ or of the form $\exists P$,
with $P$ a role. For $C=A$ setting $g_{0}(d_{A})=d$ clearly satisfies the
homomorphism property required by this lemma. For $C=\exists P$, we know that
$(d,\kappa)\in(\exists P)^{\mathcal{I}}$ holds iff there is
$d^{\prime}\in\Delta^{\mathcal{I}}$ such that $(d,d^{\prime},\kappa)\in
P^{\mathcal{I}}$. We map $d_{f}\in\Delta^{\mathcal{I}_{0}}$ (see $d_{f}$ in
the definition of the canonical model $\mathcal{I}_{C}$ for a basic concept
$C$) to such $d^{\prime}$, that is, $g_{0}(d_{f})=d^{\prime}$. Then we have
that $(d_{C},d_{f},\kappa)\in P^{\mathcal{I}_{0}}$ implies
$(g_{0}(d_{C}),g_{0}(d_{f}),\kappa)\in P^{\mathcal{I}}$, which satisfies the
homomorphism property required by this lemma. The argument for the assertions
is as in Lemma 3.13: if $(a,\kappa)\in A^{\mathcal{I}_{0}}$, then
$(A(a),\kappa)\in\mathcal{O}^{\mathbb{K}}$ so $(a^{\mathcal{I}},\kappa)\in
A^{\mathcal{I}}$, i.e. $(a,\kappa)\in A^{\mathcal{I}_{0}}$ implies
$(g_{0}(a),\kappa)\in A^{\mathcal{I}}$, and similarly for role assertions. We
have shown that $g_{0}:\mathcal{I}_{0}\rightarrow\mathcal{I}$ is a
homomorphism. The argument for the inductive step is as in Lemma 3.13. ∎

See 3.17

###### Proof.

Assume ${\mathcal{O}^{\mathbb{K}}}\models(C\sqsubseteq D,\kappa)$, where $C,D$
are basic concepts (that is, either a concept name $A$ or of the form $\exists
P$). This means that, for every interpretation $\mathcal{I}$, if
$(d,\kappa^{\prime})\in C^{\mathcal{I}}$ then
$(d,\kappa\otimes\kappa^{\prime})\in D^{\mathcal{I}}$. In particular, this
holds for the canonical model of $\mathcal{O}^{\mathbb{K}}$ and $C$. Since
$(d_{C},\mathbb{1})\in C^{\mathcal{I}_{C,\mathcal{O}^{\mathbb{K}}}}$ and
$\kappa\otimes\mathbb{1}=\kappa$ we have that $(d_{C},\kappa)\in
D^{\mathcal{I}_{C,\mathcal{O}^{\mathbb{K}}}}$. Conversely, assume
$(d_{C},\kappa)\in D^{\mathcal{I}_{C,\mathcal{O}^{\mathbb{K}}}}$. We first
state the following claim.

######  Claim A.3.

Assume $(d_{C},\kappa)\in D^{\mathcal{I}_{C,\mathcal{O}^{\mathbb{K}}}}$ and
assume $\mathcal{I}_{C,\kappa^{\prime},\mathcal{O}^{\mathbb{K}}}$ is
constructed in the same way as $\mathcal{I}_{C,\mathcal{O}^{\mathbb{K}}}$
except that we annotate the interpretation $\mathcal{I}_{C}$ of the basic
concept $C$ with $\kappa^{\prime}$ instead of $\mathbb{1}$. Then
$(d_{C},\kappa^{\prime}\otimes\kappa)\in
D^{\mathcal{I}_{C,\kappa^{\prime},\mathcal{O}^{\mathbb{K}}}}$.

###### Proof.

This is by the construction of
$\mathcal{I}_{C,\kappa^{\prime},\mathcal{O}^{\mathbb{K}}}$, which uses the
same axioms as the ones used in $\mathcal{I}_{C,\mathcal{O}^{\mathbb{K}}}$,
except that now we apply the $\otimes$ operator on $\kappa^{\prime}$ instead
of applying it on $\mathbb{1}$, and thanks to $\otimes$-idempotency which
allows us to obtain $\kappa^{\prime}\otimes\kappa$ even in the case where
$\kappa^{\prime}$ occurs several times in the product. ∎

Let $\mathcal{I}$ be a model of $\mathcal{O}^{\mathbb{K}}$. If
$(d,\kappa^{\prime})\in C^{\mathcal{I}}$, then by Lemma 3.15 there exists a
homomorphism
$g:\mathcal{I}_{C,\kappa^{\prime},\mathcal{O}^{\mathbb{K}}}\rightarrow\mathcal{I}$
such that $g(d_{C})=d$. By Claim A.3, $(d_{C},\kappa^{\prime}\otimes\kappa)\in
D^{\mathcal{I}_{C,\kappa^{\prime},\mathcal{O}^{\mathbb{K}}}}$, so by Lemma
A.1, $(d,\kappa^{\prime}\otimes\kappa)\in D^{\mathcal{I}}$. Hence
$\mathcal{I}\models(C\sqsubseteq D,\kappa)$. Since $\mathcal{I}$ was an
arbitrary model of $\mathcal{O}^{\mathbb{K}}$, we obtain
${\mathcal{O}^{\mathbb{K}}}\models(C\sqsubseteq D,\kappa)$. ∎

###  A.3 Properties on Idempotent Semirings

See 3.19

###### Proof.

Assume that $\mathcal{O}\not\models\alpha$, i.e. there is a model
$\mathcal{I}$ of $\mathcal{O}$ such that $\mathcal{I}\not\models\alpha$. By
Claim (i) of Lemma 3.6, there exists a model $\mathcal{I}^{\mathbb{K}}$ of
$\mathcal{O}^{\mathbb{K}}$ that coincides with $\mathcal{I}$ on its non-
annotated part. There is no $\kappa\in K$ such that
$\mathcal{I}^{\mathbb{K}}\models(\alpha,\kappa)$ (otherwise we would
contradict the fact that $\mathcal{I}\not\models\alpha$). It follows that
there is no $\kappa\in K$ such that
$\mathcal{O}^{\mathbb{K}}\models(\alpha,\kappa)$, thus
$\mathcal{P}(\alpha,\mathcal{O}^{\mathbb{K}})=\mathbb{0}$. Before we argue
about the other direction, we establish the following claim.

######  Claim A.4.

If
$S^{\mathbb{K}}=\\{(\alpha_{1},\kappa_{1}),\ldots,(\alpha_{n},\kappa_{n})\\}$
is a minimal subset of $\mathcal{O}^{\mathbb{K}}$ such that $S\models\alpha$
then $\mathcal{O}^{\mathbb{K}}\models(\alpha,\bigotimes^{n}_{i=1}\kappa_{i})$.

###### Proof.

We assume that $\mathcal{O}^{\mathbb{K}}$ is satisfiable (otherwise, we are
done since $\mathcal{O}^{\mathbb{K}}\models(\alpha,\chi)$ for every $\chi\in
K$). Suppose $\alpha$ is of the form $C\sqsubseteq D$, with $C,D$ basic
concepts. Assume that $C$ is satisfiable w.r.t. $\mathcal{O}$ (otherwise
$C^{\mathcal{I}}=\emptyset$ in every model $\mathcal{I}$ of
$\mathcal{O}^{\mathbb{K}}$ so $\mathcal{O}^{\mathbb{K}}\models(C\sqsubseteq
D,\chi)$ for every $\chi\in K$). Let $\mathcal{I}_{C,S}$ be the canonical
model of $C$ and $S$ (we construct it in the same way as
$\mathcal{I}_{C,S^{\mathbb{K}}}$ except that we do not have the annotations).
Since $S\models\alpha$ and $S$ is a minimal set of axioms that entails
$\alpha$, by construction of $\mathcal{I}_{C,S}$, there is a sequence
$(\alpha_{1},\mathcal{I}^{1}_{C,S}),\ldots,(\alpha_{m},\mathcal{I}^{m}_{C,S})$
of axioms and interpretations such that $d_{C}\in D^{\mathcal{I}^{m}_{C,S}}$,
where the definition of $\mathcal{I}^{j}_{C,S}$ is based on the definition of
$\mathcal{I}^{j-1}_{C,S}$ and the application of axiom $\alpha_{j}$. By
minimality of $S$ all axioms in $S$ occur in this sequence. By construction of
$\mathcal{I}_{C,S^{\mathbb{K}}}$, we have an analogous sequence
$((\alpha_{1},\kappa_{1}),\mathcal{I}^{1}_{C,S^{\mathbb{K}}}),\ldots,((\alpha_{m},\kappa_{m}),\mathcal{I}^{m}_{C,S^{\mathbb{K}}})$,
with the same axioms in $S$ except that now they are annotated, and we have
$(d_{C},\kappa)\in D^{\mathcal{I}^{m}_{C,S^{\mathbb{K}}}}$ with
$\kappa=\bigotimes^{m}_{i=1}\kappa_{i}$. Since $\mathbb{K}$ is
$\otimes$-idempotent, we have that $\kappa=\bigotimes^{n}_{i=1}\kappa_{i}$. By
Theorem 3.17, $S^{\mathbb{K}}\models(C\sqsubseteq D,\kappa)$. Since
$S^{\mathbb{K}}$ is a subset of $\mathcal{O}^{\mathbb{K}}$, by the semantics
of $\mathbb{K}$-annotated ${\cal E\\!LHI}_{\bot}$, we have that
$\mathcal{O}^{\mathbb{K}}\models S^{\mathbb{K}}\models(C\sqsubseteq
D,\kappa)$, which means that $\mathcal{O}^{\mathbb{K}}\models(C\sqsubseteq
D,\kappa)$.

Now suppose that $\alpha$ is a BCQ (or an assertion) and let
$\mathcal{I}_{S^{\mathbb{K}}}$ be the canonical model of $S^{\mathbb{K}}$. As
in the GCI case, we can obtain a sequence
$((\alpha_{1},\kappa_{1}),\mathcal{I}^{1}_{S^{\mathbb{K}}}),\ldots,((\alpha_{m},\kappa_{m}),\mathcal{I}^{m}_{S^{\mathbb{K}}})$
where the definition of $\mathcal{I}^{j}_{S^{\mathbb{K}}}$ is based on the
definition of $\mathcal{I}^{j-1}_{S^{\mathbb{K}}}$ and the application of
axiom $(\alpha_{j},\kappa_{j})$ and
$\mathcal{I}^{m}_{S^{\mathbb{K}}}\models(\alpha,\kappa)$ with
$\kappa=\bigotimes^{m}_{i=1}\kappa_{i}=\bigotimes^{n}_{i=1}\kappa_{i}$. Then
by Theorem 3.14, we obtain $S^{\mathbb{K}}\models(\alpha,\kappa)$ and
$\mathcal{O}^{\mathbb{K}}\models(\alpha,\kappa)$. ∎

Assume that $\mathbb{K}$ is positive and
$\mathcal{P}(\alpha,\mathcal{O}^{\mathbb{K}})=\mathbb{0}$. Since $\mathbb{K}$
is positive, $\mathcal{P}(\alpha,\mathcal{O}^{\mathbb{K}})=\mathbb{0}$ means
that ($\dagger$) there is no $\kappa\in K$ such that
$\mathcal{O}^{\mathbb{K}}\models(\alpha,\kappa)$ and $\kappa\neq\mathbb{0}$.
Assume for a contradiction that $\mathcal{O}\models\alpha$. Then, there is a
minimial subset
$S^{\mathbb{K}}=\\{(\alpha_{1},\kappa_{1}),\ldots,(\alpha_{n},\kappa_{n})\\}$
of $\mathcal{O}^{\mathbb{K}}$ such that $S\models\alpha$. By Claim A.4,
$\mathcal{O}^{\mathbb{K}}\models(\alpha,\bigotimes^{n}_{i=1}\kappa_{i})$.
Since $\mathbb{K}$ is positive and every $\kappa_{i}$ is different from
$\mathbb{0}$ by definition of annotated ontologies, then
$\bigotimes^{n}_{i=1}\kappa_{i}\neq\mathbb{0}$, which contradicts ($\dagger$).
∎

See 3.22

###### Proof.

Let $\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}$ be the canonical model of
$\mathcal{O}^{\mathbb{K}}$. By Theorem 3.14, for every $\kappa\in K$, we have
that $\mathcal{O}^{\mathbb{K}}\models(q,\kappa)$ iff
$\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}\models(q,\kappa)$. Hence
$\mathcal{P}(q,\mathcal{O}^{\mathbb{K}})=\bigoplus_{\mathcal{O}^{\mathbb{K}}\models(q,\kappa)}\kappa=\bigoplus_{\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}\models(q,\kappa)}\kappa$.

Let $\Pi(q,\mathcal{O})$ be the set of all matches of $q$ in $\mathcal{O}$ and
let $\boldsymbol{q}$ be the extended version of $q$. Note that $q$ is a BCQ,
hence constructed by a single disjunct. We prove that

$\\{\kappa\mid\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}\models(q,\kappa)\\}=\\{\bigotimes_{P(\vec{t})\in
q}\lambda(\pi(P(\vec{t})))\mid\pi\in\Pi(q,\mathcal{O})\\}.$

The result follows immediately from this and the idempotency of $\oplus$.
Indeed, the semiring addition will sum the same class of elements, and it
becomes irrelevant whether an element appears multiple times in the sum
$\mathcal{P}_{DB}(q,\mathcal{O}^{\mathbb{K}})=\bigoplus_{\pi\in\Pi(q,\mathcal{O})}\bigotimes_{P(\vec{t})\in
q}\lambda(\pi(P(\vec{t})))$.

Since $\mathcal{O}^{\mathbb{K}}$ contains only assertions, by construction of
$\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}$, for every $A\in{\sf N_{C}}$ it holds
that $A^{\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}}=\\{(a,\lambda(A(a)))\mid
A(a)\in\mathcal{O}\\}$ and similarly for every $R\in{\sf N_{R}}$ it holds that
$R^{\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}}=\\{(a,b,\lambda(R(a,b)))\mid
R(a,b)\in\mathcal{O}\\}$.

[“$\subseteq$”] Let $\kappa$ be s.t.
$\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}\models(q,\kappa)$. There is a match
$\pi$ of $\boldsymbol{q}$ in $\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}$ s.t.
$\kappa=\bigotimes_{P(\vec{t},t)\in\boldsymbol{q}}\pi(t)$. It is easy to see
that $\pi\in\Pi(q,\mathcal{O})$, and that for every $P(\vec{t})\in q$ with
$P(\vec{t},t)\in\boldsymbol{q}$, $\lambda(\pi(P(\vec{t})))=\pi(t)$. Hence
$\kappa\in\\{\bigotimes_{P(\vec{t})\in
q}\lambda(\pi(P(\vec{t})))\mid\pi\in\Pi(q,\mathcal{O})\\}$.

[“$\supseteq$”] Given a match $\pi\in\Pi(q,\mathcal{O})$, the function
$\pi^{\prime}$ which for every $P(\vec{t},t)\in\boldsymbol{q}$ maps $\vec{t}$
to $\pi(\vec{t})$ and $t$ to $\lambda(\pi(P(\vec{t})))$ is a match of
$\boldsymbol{q}$ in $\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}$. Thus, for every
match $\pi\in\Pi(q,\mathcal{O})$, it holds that $\bigotimes_{P(\vec{t})\in
q}\lambda(\pi(P(\vec{t})))\in\\{\kappa\mid\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}\models(q,\kappa)\\}$.
∎

See 3.24

###### Proof.

We denote by $\mathcal{D}^{\mathbb{K}}=\langle\mathcal{D},\lambda\rangle$ the
annotated database corresponding to the assertions in
$\mathcal{O}^{\mathbb{K}}$ and let $\\{C_{i}\sqsubseteq A\mid 1\leq i\leq
n\\}$ be the set of all GCIs in $\mathcal{O}$ and $\Pi(q_{C_{i}},\mathcal{D})$
be the set of all matches of the query $q_{C_{i}}(a)$ in $\mathcal{D}$; $1\leq
i\leq n$. Let $\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}$ be the canonical model
of $\mathcal{O}^{\mathbb{K}}$. Since $\mathcal{O}^{\mathbb{K}}$ contains only
assertions and GCIs of the form $C_{i}\sqsubseteq A$ labelled with
$\mathbb{1}$ where $C_{i}$ does not contain $A$, by construction of
$\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}$, it holds that

  * •

$B^{\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}}=\\{(b,\lambda(B(b)))\mid
B(b)\in\mathcal{D}\\}$, for every $B\in{\sf N_{C}}\setminus\\{A\\}$;

  * •

$R^{\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}}=\\{(b,c,\lambda(R(b,c)))\mid
R(b,c)\in\mathcal{D}\\}$, for every $R\in{\sf N_{R}}$; and

  * •

$A^{\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}}=\\{(b,\lambda(A(b)))\mid
A(b)\in\mathcal{D}\\}\cup\bigcup_{i=1}^{n}C_{i}^{\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}}$.

By Lemma 3.9,
$\\{\kappa\mid(d,\kappa)\in{C_{i}}^{\mathcal{I}}\\}=\\{\bigotimes_{P(\vec{t},t)\in\boldsymbol{q_{C_{i}}}(x)}\pi(t)\mid\pi\in\nu_{\mathcal{I}}(\boldsymbol{q_{C_{i}}}(x)),\pi(x)=d\\}$,
where $\boldsymbol{q_{C_{i}}}(x)$ is the extended version of ${q_{C_{i}}}(x)$
($1\leq i\leq n$). Hence,

$A^{\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}}=\\{(b,\lambda(A(b)))\mid
A(b)\in\mathcal{D}\\}\cup\bigcup_{i=1}^{n}\\{(b,\bigotimes_{P(\vec{t},t)\in\boldsymbol{q_{C_{i}}}(b)}\pi(t))\mid\pi\in\nu_{\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}}(\boldsymbol{q_{C_{i}}}(b))\\}.$

It follows that

$\displaystyle\\{\kappa\mid\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}\models(A(a),\kappa)\\}=$
$\displaystyle\\{\lambda(A(a))\mid
A(a)\in\mathcal{D}\\}\cup\bigcup_{i=1}^{n}\\{\bigotimes_{P(\vec{t},t)\in\boldsymbol{q_{C_{i}}}(a)}\pi(t))\mid\pi\in\nu_{\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}}(\boldsymbol{q_{C_{i}}}(a))\\}$
$\displaystyle=$
$\displaystyle\left\\{\lambda(\pi(A(a)))\mid\pi\in\Pi(A(a),\mathcal{D})\right\\}\cup$
$\displaystyle\bigcup_{i=1}^{n}\left\\{\bigotimes_{P(\vec{t})\in
q_{C_{i}}(a)}\lambda(\pi(P(\vec{t})))\mid\pi\in\Pi(q_{C_{i}},\mathcal{D})\right\\}.$

As in the proof of Theorem 3.22,
$\mathcal{P}(A(a),\mathcal{O}^{\mathbb{K}})=\bigoplus_{\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}\models(A(a),\kappa)}\kappa$
(by Theorem 3.14) and the result follows immediately from the equality above
and idempotency of $\oplus$. ∎

See 3.27

###### Proof.

We denote by $\boldsymbol{q}$ the extended version of $q$. We show that

$\bigcap_{\mathcal{I}\models\mathcal{O}^{\mathbb{K}}}{\sf
prov}_{\mathcal{I}}({\boldsymbol{q}})=\bigcap_{(I,\mu^{I})\models(\Sigma,\mathcal{D}^{\mathbb{K}})}\mu^{I}(\mathsf{goal}),$

so that

$\mathcal{P}(q,\mathcal{O}^{\mathbb{K}})=\bigoplus_{\kappa\in\bigcap_{\mathcal{I}\models\mathcal{O}^{\mathbb{K}}}{\sf
prov}_{\mathcal{I}}({\boldsymbol{q}})}\kappa=\bigoplus_{\kappa\in\bigcap_{(I,\mu^{I})\models(\Sigma,\mathcal{D}^{\mathbb{K}})}\mu^{I}(\mathsf{goal})}\kappa=\mathcal{P}_{Dat}^{\texttt{SAM}}(\Sigma,\mathcal{D}^{\mathbb{K}},\mathsf{goal}).$

[“$\supseteq$”] For every $\mathcal{I}$ such that
$\mathcal{I}\models\mathcal{O}^{\mathbb{K}}$, we define
$f(\mathcal{I})=(I,\mu^{I})$ by
$I=\\{A(a)\mid\exists\kappa,\mathcal{I}\models(A(a),\kappa)\\}\cup\\{R(a,b)\mid\exists\kappa,\mathcal{I}\models(R(a,b),\kappa)\\}\cup\\{F_{\alpha}\mid\alpha\text{
GCI or RI of
}\mathcal{O}\\}\cup\\{\mathsf{goal}\mid\mathcal{I}\models\boldsymbol{q}\\}$,
and $\mu^{I}(\alpha)={\sf prov}_{\mathcal{I}}({\alpha})$ if $\alpha$ is an
assertion, $\mu^{I}(F_{\alpha})=\\{\lambda(\alpha)\\}$ if $\alpha$ is a GCI or
an RI, and $\mu^{I}(\mathsf{goal})={\sf
prov}_{\mathcal{I}}({\boldsymbol{q}})=\\{\bigotimes_{P(\vec{t},t)\in\boldsymbol{q}}\pi(t)\mid\pi\in\nu_{\mathcal{I}}(\boldsymbol{q})\\}$.
We show that $f(\mathcal{I})\models(\Sigma,\mathcal{D}^{\mathbb{K}})$.

  1. 1.

Since $\mathcal{I}$ satisfies every annotated assertion of
$\mathcal{O}^{\mathbb{K}}$, it is easy to check that $\mathcal{D}\subseteq I$,
that for every $\alpha\in\mathcal{D}\cap\mathcal{O}$,
$\lambda^{\prime}(\alpha)=\lambda(\alpha)$ belongs to $\mu^{I}(\alpha)={\sf
prov}_{\mathcal{I}}({\alpha})$ and that for every
$F_{\alpha}\in\mathcal{D}\setminus\mathcal{O}$,
$\lambda^{\prime}(F_{\alpha})=\lambda(\alpha)$ belongs to
$\mu^{I}(F_{\alpha})=\\{\lambda(\alpha)\\}$.

  2. 2.

Let $\phi(\vec{x},\vec{y})\rightarrow H(\vec{x})\in\Sigma$ be such that there
is a homomorphism $h:\phi(\vec{x},\vec{y})\mapsto I$. We consider the case
where $\phi(\vec{x},\vec{y})\rightarrow H(\vec{x})$ corresponds to an
annotated GCI $(C\sqsubseteq A,\kappa^{\prime})\in\mathcal{O}^{\mathbb{K}}$
(the case of role inclusion is similar): $\phi(\vec{x},\vec{y})\rightarrow
H(\vec{x})$ is of the form $q_{C}(x)\wedge F_{C\sqsubseteq A}\rightarrow
A(x)$. Assume that $h(q_{C}(x))=\beta_{1}\wedge\dots\wedge\beta_{n}$. By
construction of $I$ and $\mu^{I}$, for every $1\leq i\leq n$, since
$\beta_{i}\in I$, $\mu^{I}(\beta_{i})\neq\emptyset$ and for every
$\kappa_{i}\in\mu^{I}(\beta_{i})$, $\mathcal{I}\models(\beta_{i},\kappa_{i})$.
By Lemma 3.9,
$\\{\bigotimes_{P(\vec{t},t)\in\boldsymbol{q_{C}}(x)}\pi(t)\mid\pi\in\nu_{\mathcal{I}}(\boldsymbol{q_{C}}(x)),\pi(x)=h(x)^{\mathcal{I}}\\}=\\{\kappa\mid(h(x)^{\mathcal{I}},\kappa)\in
C^{\mathcal{I}}\\}$ where $\boldsymbol{q_{C}}$ is the extended version of
$q_{C}$. For every
$(\kappa_{1},\dots,\kappa_{n})\in\mu^{I}(\beta_{1})\times\dots\times\mu^{I}(\beta_{n})$,
there is $\pi\in\nu_{\mathcal{I}}(\boldsymbol{q_{C}}(x))$ such that $\pi$ maps
$\boldsymbol{q_{C}}(x)$ to
$\\{(\beta_{1},\kappa_{1}),\dots,(\beta_{n},\kappa_{n})\\}$, so
$(h(x)^{\mathcal{I}},\kappa_{1}\otimes\dots\otimes\kappa_{n})\in
C^{\mathcal{I}}$. Since $\mathcal{I}\models(C\sqsubseteq A,\kappa^{\prime})$,
then
$(h(x)^{\mathcal{I}},\kappa_{1}\otimes\dots\otimes\kappa_{n}\otimes\kappa^{\prime})\in
A^{\mathcal{I}}$. It follows that $h(A(x))\in I$ and
$\\{\bigotimes_{i=1}^{n+1}\kappa_{i}\mid(\kappa_{1},\dots,\kappa_{n},\kappa_{n+1})\in\mu^{I}(\beta_{1})\times\dots\times\mu^{I}(\beta_{n})\times\mu^{I}(F_{C\sqsubseteq
A})\\}\subseteq\mu^{I}(h(A(x)))$ (since $\mu^{I}(F_{C\sqsubseteq
A})=\\{\kappa^{\prime}\\}$ by definition of $\mu^{I}$).

$\text{Hence }\bigcap_{\mathcal{I}\models\mathcal{O}^{\mathbb{K}}}{\sf
prov}_{\mathcal{I}}({\boldsymbol{q}})\
=\bigcap_{\mathcal{I}\models\mathcal{O}^{\mathbb{K}},f(\mathcal{I})=(I,\mu^{I})}\mu^{I}(\mathsf{goal})\
\supseteq\
\bigcap_{(I,\mu^{I})\models(\Sigma,\mathcal{D}^{\mathbb{K}})}\mu^{I}(\mathsf{goal}).$

[“$\subseteq$”] For every $(I,\mu^{I})$ s.t.
$(I,\mu^{I})\models(\Sigma,\mathcal{D}^{\mathbb{K}})$, we define
$g(I,\mu^{I})=(\Delta^{\mathcal{I}},K,\cdot^{\mathcal{I}})$ by
$\Delta^{\mathcal{I}}={\sf N_{I}}$, $a^{\mathcal{I}}=a$ for every $a\in{\sf
N_{I}}$, $A^{\mathcal{I}}=\\{(a,\kappa)\mid A(a)\in
I,\kappa\in\mu^{I}(A(a))\\}$ and $R^{\mathcal{I}}=\\{(a,b,\kappa)\mid
R(a,b)\in I,\kappa\in\mu^{I}(R(a,b))\\}$. We show that
$g(I,\mu^{I})\models\mathcal{O}^{\mathbb{K}}$ and that ${\sf
prov}_{\mathcal{I}}({\boldsymbol{q}})\subseteq\mu^{I}(\mathsf{goal})$.

  * •

Since $\mathcal{D}\subseteq I$ and for every $\alpha\in\mathcal{D}$,
$\lambda^{\prime}(\alpha)\in\mu^{I}(\alpha)$, since
$\lambda^{\prime}(\alpha)=\lambda(\alpha)$ for every assertion of
$\mathcal{O}$, it is easy to check that $\mathcal{I}$ satisfies every
annotated assertion of $\mathcal{O}^{\mathbb{K}}$.

  * •

Let $(C\sqsubseteq A,\kappa^{\prime})$ be an annotated GCI of
$\mathcal{O}^{\mathbb{K}}$ (the case of RI is similar). Let $(e,\kappa)\in
C^{\mathcal{I}}$ and $\boldsymbol{q_{C}}$ be the extended version of $q_{C}$.
By Lemma 3.9,
$\\{\bigotimes_{P(\vec{t},t)\in\boldsymbol{q_{C}}(x)}\pi(t)\mid\pi\in\nu_{\mathcal{I}}(\boldsymbol{q_{C}}(x)),\pi(x)=e\\}=\\{\kappa\mid(e,\kappa)\in
C^{\mathcal{I}}\\}$, so there exist
$\pi\in\nu_{\mathcal{I}}(\boldsymbol{q_{C}}(x))$ such that $\pi(x)=e$ and
$\bigotimes_{P(\vec{t},t)\in\boldsymbol{q_{C}}(x)}\pi(t)=\kappa$. Let
$(\beta_{1},\kappa_{1}),\dots,(\beta_{n},\kappa_{n})$ be the image of
$\boldsymbol{q_{C}}(x)$ by $\pi$ and $h$ be the restriction of $\pi$ to the
non-annotated part of $\mathcal{I}$. By construction,
$\kappa=\kappa_{1}\otimes\dots\otimes\kappa_{n}$ and for $1\leq i\leq n$,
$\beta_{i}\in I$, $\kappa_{i}\in\mu^{I}(\beta_{i})$, and $h$ is a homomorphism
from $q_{C}$ to $I$ such that
$h(q_{C}(x))=\beta_{1}\wedge\dots\wedge\beta_{n}$ and $h(x)=e$.

Since $q_{C}(x)\wedge F_{C\sqsubseteq A}\rightarrow A(x)$ is in $\Sigma$ and
$h$ is a homomorphism from $q_{C}(x)\wedge F_{C\sqsubseteq A}$ to $I$, since
$(I,\mu^{I})\models(\Sigma,\mathcal{D}^{\mathbb{K}})$, it follows that
$A(e)\in I$ and
$\kappa_{1}\otimes\dots\otimes\kappa_{n}\otimes\kappa^{\prime}$ is in
$\mu^{I}(A(e))$, i.e. $(e,\kappa\otimes\kappa^{\prime})\in A^{\mathcal{I}}$.
Hence $\mathcal{I}\models(C\sqsubseteq A,\kappa^{\prime})$.

  * •

Let $\kappa\in{\sf
prov}_{\mathcal{I}}({\boldsymbol{q}})=\\{\bigotimes_{P(\vec{t},t)\in\boldsymbol{q}}\pi(t)\mid\pi\in\nu_{\mathcal{I}}(\boldsymbol{q})\\}$.
There is a mapping $\pi$ from $\boldsymbol{q}$ to $\mathcal{I}$ such that
$\kappa=\bigotimes_{P(\vec{t},t)\in\boldsymbol{q}}\pi(t)$. By construction of
$\mathcal{I}$, this means that for each $P(\vec{t},t)\in\boldsymbol{q}$,
$\pi(P(\vec{t}))\in I$ and $\pi(t)\in\mu^{I}(\pi(P(\vec{t})))$. Since
$q\rightarrow\mathsf{goal}$ is in $\Sigma$ and $\pi$ is a homomorphism from
$q$ to $I$, since $(I,\mu^{I})\models(\Sigma,\mathcal{D}^{\mathbb{K}})$, it
follows that $\mathsf{goal}\in I$ and
$\bigotimes_{P(\vec{t},t)\in\boldsymbol{q}}\pi(t)\in\mu^{I}(\mathsf{goal})$.
Hence $\kappa\in\mu^{I}(\mathsf{goal})$ and ${\sf
prov}_{\mathcal{I}}({\boldsymbol{q}})\subseteq\mu^{I}(\mathsf{goal})$.

$\text{Hence }\bigcap_{\mathcal{I}\models\mathcal{O}^{\mathbb{K}}}{\sf
prov}_{\mathcal{I}}({\boldsymbol{q}})\
\subseteq\bigcap_{(I,\mu^{I})\models(\Sigma,\mathcal{D}^{\mathbb{K}}),g(I,\mu^{I})=\mathcal{I}}{\sf
prov}_{\mathcal{I}}({\boldsymbol{q}})\
\subseteq\bigcap_{(I,\mu^{I})\models(\Sigma,\mathcal{D}^{\mathbb{K}})}\mu^{I}(\mathsf{goal}).\qed$

See 3.28

###### Proof.

Let $\mathcal{O}$ be a satisfiable ${\cal E\\!LHI}_{\bot}$ ontology with
annotated versions
$\mathcal{O}^{\mathbb{K}_{1}}=\langle\mathcal{O},\lambda\rangle$ and
$\mathcal{O}^{\mathbb{K}_{2}}=\langle\mathcal{O},h\circ\lambda\rangle$, where
$\mathbb{K}_{1}=(K_{1},\oplus,\otimes,\mathbb{0},\mathbb{1})$ and
$\mathbb{K}_{2}=(K_{2},+,\cdot,0,1)$ are commutative additively idempotent
$\omega$-continuous semirings.

$\mathcal{O}^{\mathbb{K}_{1}}=\\{(\alpha,\lambda(\alpha))\mid\alpha\in\mathcal{O}\\}\text{
and
}\mathcal{O}^{\mathbb{K}_{2}}=\\{(\alpha,h(\lambda(\alpha)))\mid\alpha\in\mathcal{O}\\}.$

Recall that since $\mathcal{O}$ is satisfiable, by Lemma 3.6,
$\mathcal{O}^{\mathbb{K}_{1}}$ and $\mathcal{O}^{\mathbb{K}_{2}}$ are
satisfiable. Recall also that since $h$ is a semiring homomorphism,
$h(\mathbb{0})=0$, $h(\mathbb{1})=1$, and for all $a,b\in K_{1}$, $h(a\oplus
b)=h(a)+h(b)$ and $h(a\otimes b)=h(a)\cdot h(b)$, and since it is
$\omega$-continuous, it preserves least upper bounds
($h(\sup((a_{i})_{i\in\mathbb{N}}))=\sup((h(a_{i}))_{i\in\mathbb{N}})$).

######  Claim A.5.

Let $\mathcal{O}^{\mathbb{K}_{1}}=\langle\mathcal{O},\lambda\rangle$ and
$\mathcal{O}^{\mathbb{K}_{2}}=\langle\mathcal{O},h\circ\lambda\rangle$ be as
in this proof.

  * •

For every assertion or BCQ $\alpha$, for every $\kappa\in K_{1}$, if
$\mathcal{O}^{\mathbb{K}_{1}}\models(\alpha,\kappa)$ then
$\mathcal{O}^{\mathbb{K}_{2}}\models(\alpha,h(\kappa))$.

  * •

If $\mathbb{K}_{1}$ and $\mathbb{K}_{2}$ are also multiplicatively idempotent
then, for every GCI $\alpha$ between basic concepts satisfiable w.r.t.
$\mathcal{O}$, for every $\kappa\in K_{1}$, if
$\mathcal{O}^{\mathbb{K}_{1}}\models(\alpha,\kappa)$ then
$\mathcal{O}^{\mathbb{K}_{2}}\models(\alpha,h(\kappa))$.

Let $\mathcal{I}_{\mathcal{O}^{\mathbb{K}_{1}}}$ and
$\mathcal{I}_{\mathcal{O}^{\mathbb{K}_{2}}}$ be the canonical models of
$\mathcal{O}^{\mathbb{K}_{1}}$ and $\mathcal{O}^{\mathbb{K}_{2}}$,
respectively (see Section 3.4 for the definition). First assume $\alpha$ is an
assertion or BCQ. By Theorem 3.14, if
$\mathcal{O}^{\mathbb{K}_{1}}\models(\alpha,\kappa)$ then
$\mathcal{I}_{\mathcal{O}^{\mathbb{K}_{1}}}\models(\alpha,\kappa)$. By
definition of $\mathcal{O}^{\mathbb{K}_{2}}$, the canonical model
$\mathcal{I}_{\mathcal{O}^{\mathbb{K}_{2}}}$ has the same construction as
$\mathcal{I}_{\mathcal{O}^{\mathbb{K}_{1}}}$, except for the annotations
$\kappa$ which are $h(\kappa)$ in
$\mathcal{I}_{\mathcal{O}^{\mathbb{K}_{2}}}$. Then,
$\mathcal{I}_{\mathcal{O}^{\mathbb{K}_{2}}}\models(\alpha,h(\kappa))$ and, by
Theorem 3.14, $\mathcal{O}^{\mathbb{K}_{2}}\models(\alpha,h(\kappa))$.

Now assume $\alpha$ is of the form $C\sqsubseteq D$, with $C,D$ basic concepts
satisfiable w.r.t. $\mathcal{O}$ and that $\mathbb{K}_{1}$ and
$\mathbb{K}_{2}$ are multiplicatively idempotent. Let
$\mathcal{I}_{C,\mathcal{O}^{\mathbb{K}_{i}}}$ be the canonical model of $C$
and $\mathcal{O}^{\mathbb{K}_{i}}$ with $i\in\\{1,2\\}$ (see Section 3.4 for
the definition). By Theorem 3.17, if
$\mathcal{O}^{\mathbb{K}_{1}}\models(C\sqsubseteq D,\kappa)$ then
$(d_{C},\kappa)\in D^{\mathcal{I}_{C,\mathcal{O}^{\mathbb{K}_{1}}}}$. By
definition of $\mathcal{O}^{\mathbb{K}_{2}}$, the canonical model
$\mathcal{I}_{C,\mathcal{O}^{\mathbb{K}_{2}}}$ has the same construction as
$\mathcal{I}_{C,\mathcal{O}^{\mathbb{K}_{1}}}$, except for the annotations
$\kappa$ which are $h(\kappa)$ in
$\mathcal{I}_{C,\mathcal{O}^{\mathbb{K}_{2}}}$. Then, $(d_{C},h(\kappa))\in
D^{\mathcal{I}_{C,\mathcal{O}^{\mathbb{K}_{2}}}}$ and, by Theorem 3.17, we
have that $\mathcal{O}^{\mathbb{K}_{2}}\models(C\sqsubseteq D,h(\kappa))$.

######  Claim A.6.

Let $\mathcal{O}^{\mathbb{K}_{1}}=\langle\mathcal{O},\lambda\rangle$ and
$\mathcal{O}^{\mathbb{K}_{2}}=\langle\mathcal{O},h\circ\lambda\rangle$ be as
in this proof.

  * •

For every assertion or BCQ $\alpha$, for every $\kappa^{\prime}\in K_{2}$, if
$\mathcal{O}^{\mathbb{K}_{2}}\models(\alpha,\kappa^{\prime})$ then there
exists $\kappa\in K_{1}$ such that $h(\kappa)=\kappa^{\prime}$ and
$\mathcal{O}^{\mathbb{K}_{1}}\models(\alpha,\kappa)$.

  * •

If $\mathbb{K}_{1}$ and $\mathbb{K}_{2}$ are also multiplicatively idempotent
then, for every GCI $\alpha$ between basic concepts satisfiable w.r.t.
$\mathcal{O}$, for every $\kappa^{\prime}\in K_{2}$, if
$\mathcal{O}^{\mathbb{K}_{2}}\models(\alpha,\kappa^{\prime})$ then there
exists $\kappa\in K_{1}$ such that $h(\kappa)=\kappa^{\prime}$ and
$\mathcal{O}^{\mathbb{K}_{1}}\models(\alpha,\kappa)$.

Let $\mathcal{I}_{\mathcal{O}^{\mathbb{K}_{1}}}$ and
$\mathcal{I}_{\mathcal{O}^{\mathbb{K}_{2}}}$ be the canonical models of
$\mathcal{O}^{\mathbb{K}_{1}}$ and $\mathcal{O}^{\mathbb{K}_{2}}$,
respectively. Assume $\alpha$ is an assertion or a BCQ. By Theorem 3.14, if
$\mathcal{O}^{\mathbb{K}_{2}}\models(\alpha,\kappa^{\prime})$ then
$\mathcal{I}_{\mathcal{O}^{\mathbb{K}_{2}}}\models(\alpha,\kappa^{\prime})$.
By definition of $\mathcal{O}^{\mathbb{K}_{2}}$, the canonical model
$\mathcal{I}_{\mathcal{O}^{\mathbb{K}_{2}}}$ has the same construction as
$\mathcal{I}_{\mathcal{O}^{\mathbb{K}_{1}}}$, except for the annotations
$\kappa^{\prime}$ for which there exists $\kappa\in K_{1}$ such that
$h(\kappa)=\kappa^{\prime}$. That is,
$\mathcal{I}_{\mathcal{O}^{\mathbb{K}_{1}}}\models(\alpha,\kappa)$ and, by
Theorem 3.14, $\mathcal{O}^{\mathbb{K}_{1}}\models(\alpha,\kappa)$.

Now assume $\alpha$ is of the form $C\sqsubseteq D$, with $C,D$ basic concepts
satisfiable w.r.t. $\mathcal{O}$ and that $\mathbb{K}_{1}$ and
$\mathbb{K}_{2}$ are multiplicatively idempotent. Let
$\mathcal{I}_{C,\mathcal{O}^{\mathbb{K}_{i}}}$ be the canonical model of $C$
and $\mathcal{O}^{\mathbb{K}_{i}}$ with $i\in\\{1,2\\}$. By Theorem 3.17, if
$\mathcal{O}^{\mathbb{K}_{2}}\models(C\sqsubseteq D,\kappa^{\prime})$ then
$(d_{C},\kappa^{\prime})\in D^{\mathcal{I}_{C,\mathcal{O}^{\mathbb{K}_{2}}}}$.
By definition of $\mathcal{O}^{\mathbb{K}_{2}}$, the canonical model
$\mathcal{I}_{C,\mathcal{O}^{\mathbb{K}_{2}}}$ has the same construction as
$\mathcal{I}_{C,\mathcal{O}^{\mathbb{K}_{1}}}$, except for the annotations
$\kappa^{\prime}$ for which there exists $\kappa\in K_{1}$ such that
$h(\kappa)=\kappa^{\prime}$. Then, $(d_{C},\kappa)\in
D^{\mathcal{I}_{C,\mathcal{O}^{\mathbb{K}_{1}}}}$ and, by Theorem 3.17,
$\mathcal{O}^{\mathbb{K}_{1}}\models(C\sqsubseteq D,\kappa)$.

By Claims A.5 and A.6, the definitions of
$\mathcal{P}(\alpha,\mathcal{O}^{\mathbb{K}_{1}})$,
$\mathcal{P}(\alpha,\mathcal{O}^{\mathbb{K}_{2}})$ and additive idempotency,

$\displaystyle\mathcal{P}(\alpha,\mathcal{O}^{\mathbb{K}_{2}})=$
$\displaystyle\mathop{\mathchoice{\vbox{\hbox{\leavevmode\resizebox{}{9.00005pt}{\raisebox{0.0pt}{$\displaystyle+$}}}}\vphantom{\sum}}{\vbox{\hbox{\leavevmode\resizebox{}{9.00005pt}{\raisebox{0.0pt}{$\textstyle+$}}}}\vphantom{\sum}}{\vbox{\hbox{\leavevmode\resizebox{}{6.30003pt}{\raisebox{0.0pt}{$\scriptstyle+$}}}}\vphantom{\sum}}{\vbox{\hbox{\leavevmode\resizebox{}{4.50002pt}{\raisebox{0.0pt}{$\scriptscriptstyle+$}}}}\vphantom{\sum}}}\slimits@_{\mathcal{O}^{\mathbb{K}_{2}}\models(\alpha,\kappa^{\prime})}\kappa^{\prime}=\mathop{\mathchoice{\vbox{\hbox{\leavevmode\resizebox{}{9.00005pt}{\raisebox{0.0pt}{$\displaystyle+$}}}}\vphantom{\sum}}{\vbox{\hbox{\leavevmode\resizebox{}{9.00005pt}{\raisebox{0.0pt}{$\textstyle+$}}}}\vphantom{\sum}}{\vbox{\hbox{\leavevmode\resizebox{}{6.30003pt}{\raisebox{0.0pt}{$\scriptstyle+$}}}}\vphantom{\sum}}{\vbox{\hbox{\leavevmode\resizebox{}{4.50002pt}{\raisebox{0.0pt}{$\scriptscriptstyle+$}}}}\vphantom{\sum}}}\slimits@_{\mathcal{O}^{\mathbb{K}_{1}}\models(\alpha,\kappa)}h(\kappa)=h(\bigoplus_{\mathcal{O}^{\mathbb{K}_{1}}\models(\alpha,\kappa)}\kappa)=h(\mathcal{P}(\alpha,\mathcal{O}^{\mathbb{K}_{1}})).\qed$

##  B Proofs for Section 4

See 4.1

###### Proof.

Given a satisfiable $\sf{Why}[{\sf X}]$-annotated ontology $\mathcal{O}$, we
denote by $\mathcal{I}_{\mathcal{O}}$ its canonical model. Since every axiom
of a $\sf{Why}[{\sf X}]$-annotated ontology is annotated with some variable
from ${\sf X}$, it follows from the construction of
$\mathcal{I}_{\mathcal{O}}$ that for every $A\in{\sf N_{C}}$, $(a,m)\in
A^{\mathcal{I}_{\mathcal{O}}}$ implies that $m$ is a product of variables from
${\sf X}$, i.e. a monomial over ${\sf X}$, and similarly for roles.

  * •

If $\alpha$ is an assertion $P(\vec{a})$, then $\mathcal{O}\models(\alpha,m)$
implies $\mathcal{I}_{\mathcal{O}}\models(P(\vec{a}),m)$, i.e. $(\vec{a},m)\in
P^{\mathcal{I}_{\mathcal{O}}}$, so $m$ is a monomial.

  * •

If $\alpha$ is a BCQ $q$ whose extended version is $\boldsymbol{q}$, then by
Theorem 3.14, $\mathcal{O}\models(\alpha,m)$ implies
$\mathcal{I}_{\mathcal{O}}\models(\alpha,m)$, i.e. $m\in{\sf
prov}_{\mathcal{I}_{\mathcal{O}}}({\boldsymbol{q}})=\\{\bigotimes_{P(\vec{t},t)\in\boldsymbol{q}}\pi(t)\mid\pi\in\nu_{\mathcal{I}_{\mathcal{O}}}(\boldsymbol{q})\\}$
where $\pi(t)$ is the last element of the tuple $\pi(\vec{t},t)\in
P^{\mathcal{I}_{\mathcal{O}}}$. Hence, since a product of monomials is a
monomial, $m$ is a monomial.

  * •

If $\alpha$ is a RI $P\sqsubseteq Q$ with $P$ a satisfiable role, let
$\mathcal{O}^{\prime}=\mathcal{O}\cup\\{(P(a,b),x)\\}$ where $a,b\in{\sf
N_{I}}$ and $x\in{\sf X}$ do not occur in $\mathcal{O}$. Since $P$ is
satisfiable, $\mathcal{O}^{\prime}$ is satisfiable, and
$\mathcal{O}\models(\alpha,m)$ implies $(a,b,x\times m)\in
Q^{\mathcal{I}_{\mathcal{O}^{\prime}}}$. Since $x\times m$ must be a monomial,
it follows that $m$ is a monomial.

  * •

If $\alpha$ is a GCI $C\sqsubseteq D$ with $C$ a satisfiable ${\cal E\\!LHI}$
concept, then by Theorem 3.17, ${\mathcal{O}^{\mathbb{K}}}\models(C\sqsubseteq
D,m)$ implies $(d_{C},m)\in D^{\mathcal{I}_{C,\mathcal{O}^{\mathbb{K}}}}$
where $\mathcal{I}_{C,\mathcal{O}^{\mathbb{K}}}$ is the canonical for $C$ and
$\mathcal{O}^{\mathbb{K}}$. Annotations in
$\mathcal{I}_{C,\mathcal{O}^{\mathbb{K}}}$ are monomials by construction, so
$m$ is a monomial. ∎

###  B.1 Annotated Axiom Entailment from ${\cal E\\!LHI}_{\bot}$ Ontologies

See 4.3

###### Proof.

For the first point, we show by induction that for every $\sf{Why}[{\sf
X}]$-annotated ${\cal E\\!LHI}_{\bot}$ ontology $\mathcal{O}$, if
$\mathcal{O}^{\prime}$ is obtained from $\mathcal{O}$ by applying $i$
normalization steps, then every model $\mathcal{I}$ of $\mathcal{O}^{\prime}$
is also a model of $\mathcal{O}$.

_Base case: $i=1$._ Let $\mathcal{O}$ be a $\sf{Why}[{\sf X}]$-annotated
${\cal E\\!LHI}_{\bot}$ and assume that $\mathcal{O}^{\prime}$ is obtained
from $\mathcal{O}$ by applying a single normalization rule $\mathsf{NF}$. We
have the three following cases.

$\mathsf{NF}=\mathsf{NF}_{1}$:

Let $\mathcal{I}$ be a model of
$\mathcal{O}^{\prime}=\mathcal{O}\setminus\\{(C\sqcap\widehat{D}\sqsubseteq
E,\,v)\\}\cup\\{(\widehat{D}\sqsubseteq A,\,1),\,(C\sqcap A\sqsubseteq
E,\,v)\\}$ and let $(d,n)\in(C\sqcap\widehat{D})^{\mathcal{I}}$. There exist
$n_{1},n_{2}\in\sf{Why}[{\sf X}]$ such that $(d,n_{1})\in C^{\mathcal{I}}$,
$(d,n_{2})\in\widehat{D}^{\mathcal{I}}$, and $n_{1}\times n_{2}=n$. Since
$\mathcal{I}\models(\widehat{D}\sqsubseteq A,1)$, then $(d,n_{2})\in
A^{\mathcal{I}}$. Hence $(d,n_{1}\times n_{2})\in(C\sqcap A)^{\mathcal{I}}$.
Since $\mathcal{I}\models(C\sqcap A\sqsubseteq E,\,v)$, it follows that
$(d,n_{1}\times n_{2}\times v)\in E^{\mathcal{I}}$, i.e., $(d,n\times v)\in
E^{\mathcal{I}}$. Thus $\mathcal{I}\models(C\sqcap\widehat{D}\sqsubseteq
E,\,v)$, and $\mathcal{I}$ is a model of $\mathcal{O}$.

$\mathsf{NF}=\mathsf{NF}_{2}$:

Let $\mathcal{I}$ be a model of
$\mathcal{O}^{\prime}=\mathcal{O}\setminus\\{(\exists P.\widehat{C}\sqsubseteq
D,\,v)\\}\cup\\{(\widehat{C}\sqsubseteq A,\,1),\,(\exists P.A\sqsubseteq
D,\,v)\\}$ and let $(d,n)\in(\exists P.\widehat{C})^{\mathcal{I}}$. There
exist $e\in\Delta^{\mathcal{I}}$ and $n_{1},n_{2}\in\sf{Why}[{\sf X}]$ such
that $(d,e,n_{1})\in P^{\mathcal{I}}$,
$(e,n_{2})\in\widehat{C}^{\mathcal{I}}$, and $n_{1}\times n_{2}=n$. Since
$\mathcal{I}\models(\widehat{C}\sqsubseteq A,\,1)$, then $(e,n_{2})\in
A^{\mathcal{I}}$. Hence $(d,n_{1}\times n_{2})\in(\exists P.A)^{\mathcal{I}}$.
Since $\mathcal{I}\models(\exists P.A\sqsubseteq D,\,v)$, it follows that
$(d,n_{1}\times n_{2}\times v)\in D^{\mathcal{I}}$, i.e. $(d,n\times v)\in
D^{\mathcal{I}}$. Thus $\mathcal{I}\models(\exists P.\widehat{C}\sqsubseteq
D,\,v)$, and $\mathcal{I}$ is a model of $\mathcal{O}$.

$\mathsf{NF}=\mathsf{NF}_{3}$:

Let $\mathcal{I}$ be a model of
$\mathcal{O}^{\prime}=\mathcal{O}\setminus\\{(\widehat{C}\sqsubseteq\exists
P,\,v)\\}\cup\\{(\widehat{C}\sqsubseteq A,\,1),\,(A\sqsubseteq\exists
P,\,v)\\}$ and let $(d,n)\in\widehat{C}^{\mathcal{I}}$. Since
$\mathcal{I}\models(\widehat{C}\sqsubseteq A,\,1)$, then $(d,n)\in
A^{\mathcal{I}}$. Since $\mathcal{I}\models(A\sqsubseteq\exists P,\,v)$, it
follows that $(d,n\times v)\in(\exists P)^{\mathcal{I}}$. Thus
$\mathcal{I}\models(\widehat{C}\sqsubseteq\exists P,\,v)$, and $\mathcal{I}$
is a model of $\mathcal{O}$.

_Induction step._ Assume that the property is true for some $i\geq 1$ and let
$\mathcal{O}$ be a $\sf{Why}[{\sf X}]$-annotated ${\cal E\\!LHI}_{\bot}$
ontology, $\mathcal{O}^{\prime}$ be the result of applying $i+1$ normalization
steps to $\mathcal{O}$ and $\mathcal{O}^{\prime\prime}$ that of applying the
first $i$ steps to $\mathcal{O}$. By applying the induction hypothesis on
$\mathcal{O}^{\prime\prime}$, we obtained that every model of
$\mathcal{O}^{\prime\prime}$ is a model of $\mathcal{O}$. Then since
$\mathcal{O}^{\prime}$ results from applying one normalization step to
$\mathcal{O}^{\prime\prime}$, we obtain that every model of
$\mathcal{O}^{\prime}$ is a model of $\mathcal{O}^{\prime\prime}$, and thus
also a model of $\mathcal{O}$.

Conversely, we show by induction that for every $i$ and for every
$\sf{Why}[{\sf X}]$-annotated ${\cal E\\!LHI}_{\bot}$ ontology $\mathcal{O}$,
if $\mathcal{O}^{\prime}$ can be obtained from $\mathcal{O}$ by applying $i$
normalization rules, then if $\mathcal{O}^{\prime}\models(\alpha,m)$ and every
concept name occurring in $\alpha$ occurs in $\mathcal{O}$, it holds that
$\mathcal{O}\models(\alpha,m)$.

_Base case: $i=1$._ Let $\mathcal{O}$ be a $\sf{Why}[{\sf X}]$-annotated
${\cal E\\!LHI}_{\bot}$, $\alpha$ be an axiom such that every concept name
occurring in $\alpha$ occurs in $\mathcal{O}$ and $m$ be a monomial. Assume
that $\mathcal{O}^{\prime}$ is obtained from $\mathcal{O}$ by applying a
normalization rule $\mathsf{NF}$ and that
$\mathcal{O}^{\prime}\models(\alpha,m)$. We have three cases.

$\mathsf{NF}=\mathsf{NF}_{1}$:

$\mathcal{O}^{\prime}=\mathcal{O}\setminus\\{(C\sqcap\widehat{D}\sqsubseteq
E,\,v)\\}\cup\\{(\widehat{D}\sqsubseteq A,\,1),\,(C\sqcap A\sqsubseteq
E,\,v)\\}$. Let $\mathcal{I}$ be a model of $\mathcal{O}$ and $\mathcal{J}$ be
the interpretation that extends $\mathcal{I}$ with
$A^{\mathcal{J}}=\widehat{D}^{\mathcal{I}}$. Clearly,
$\mathcal{J}\models(\widehat{D}\sqsubseteq A,\,1)$. Let $(d,n)\in(C\sqcap
A)^{\mathcal{J}}$. There exist $n_{1},n_{2}\in\sf{Why}[{\sf X}]$ such that
$(d,n_{1})\in C^{\mathcal{J}}=C^{\mathcal{I}}$, $(d,n_{2})\in
A^{\mathcal{J}}=\widehat{D}^{\mathcal{I}}$, and $n_{1}\times n_{2}=n$. It
follows that $(d,n_{1}\times n_{2})\in(C\sqcap\widehat{D})^{\mathcal{I}}$.
Since $\mathcal{I}\models(C\sqcap\widehat{D}\sqsubseteq E,\,v)$, it follows
that $(d,n_{1}\times n_{2}\times v)\in E^{\mathcal{I}}=E^{\mathcal{J}}$, i.e.
$(d,n\times v)\in E^{\mathcal{J}}$. Hence $\mathcal{J}\models(C\sqcap
A\sqsubseteq E,\,v)$ and $\mathcal{J}$ is a model of $\mathcal{O}^{\prime}$.
It follows that $\mathcal{J}\models(\alpha,m)$. Since $\alpha$ does not
contain $A$, then $\mathcal{I}\models(\alpha,m)$. Hence
$\mathcal{O}\models(\alpha,m)$.

$\mathsf{NF}=\mathsf{NF}_{2}$:

$\mathcal{O}^{\prime}=\mathcal{O}\setminus\\{(\exists P.\widehat{C}\sqsubseteq
D,\,v)\\}\cup\\{(\widehat{C}\sqsubseteq A,\,1),\,(\exists P.A\sqsubseteq
D,\,v)\\}$. Let $\mathcal{I}$ be a model of $\mathcal{O}$ and $\mathcal{J}$ be
the interpretation that extends $\mathcal{I}$ with
$A^{\mathcal{J}}=\widehat{C}^{\mathcal{I}}$. Clearly,
$\mathcal{J}\models(\widehat{C}\sqsubseteq A,\,1)$. Let $(d,n)\in(\exists
P.A)^{\mathcal{J}}$. There exist $e\in\Delta^{\mathcal{J}}$ and
$n_{1},n_{2}\in\sf{Why}[{\sf X}]$ such that $(d,e,n_{1})\in
P^{\mathcal{J}}=P^{\mathcal{I}}$, $(e,n_{2})\in
A^{\mathcal{J}}=\widehat{C}^{\mathcal{I}}$, and $n_{1}\times n_{2}=n$. It
follows that $(d,n_{1}\times n_{2})\in(\exists P.\widehat{C})^{\mathcal{I}}$.
Since $\mathcal{I}\models(\exists P.\widehat{C}\sqsubseteq D,\,v)$, it follows
that $(d,n_{1}\times n_{2}\times v)\in D^{\mathcal{I}}=D^{\mathcal{J}}$, i.e.
$(d,n\times v)\in D^{\mathcal{J}}$. Hence $\mathcal{J}\models(\exists
P.A\sqsubseteq D,\,v)$ and $\mathcal{J}$ is a model of $\mathcal{O}^{\prime}$.
It follows that $\mathcal{J}\models(\alpha,m)$. Since $\alpha$ does not
contain $A$, then $\mathcal{I}\models(\alpha,m)$. Hence
$\mathcal{O}\models(\alpha,m)$.

$\mathsf{NF}=\mathsf{NF}_{3}$:

$\mathcal{O}^{\prime}=\mathcal{O}\setminus\\{(\widehat{C}\sqsubseteq\exists
P,\,v)\\}\cup\\{(\widehat{C}\sqsubseteq A,\,1),\,(A\sqsubseteq\exists
P,\,v)\\}$. Let $\mathcal{I}$ be a model of $\mathcal{O}$ and $\mathcal{J}$ be
the interpretation that extends $\mathcal{I}$ with
$A^{\mathcal{J}}=\widehat{C}^{\mathcal{I}}$. Clearly,
$\mathcal{J}\models(\widehat{C}\sqsubseteq A,\,1)$. Let $(d,n)\in
A^{\mathcal{J}}=\widehat{C}^{\mathcal{I}}$. Since
$\mathcal{I}\models(\widehat{C}\sqsubseteq\exists P,\,v)$, it follows that
$(d,n\times v)\in(\exists P)^{\mathcal{I}}=(\exists P)^{\mathcal{J}}$. Hence
$\mathcal{J}\models(A\sqsubseteq\exists P,\,v)$ and $\mathcal{J}$ is a model
of $\mathcal{O}^{\prime}$. It follows that $\mathcal{J}\models(\alpha,m)$.
Since $\alpha$ does not contain $A$, then $\mathcal{I}\models(\alpha,m)$.
Hence $\mathcal{O}\models(\alpha,m)$.

_Induction step._ Assume that the property is true for some $i$ and let
$\mathcal{O}$ be a $\sf{Why}[{\sf X}]$-annotated ${\cal E\\!LHI}_{\bot}$
ontology, $\alpha$ be an axiom such that every concept name occurring in
$\alpha$ occurs in $\mathcal{O}$ and $m$ be a monomial. Let
$\mathcal{O}_{i+1}$ be obtained by applying $i+1$ normalization rules to
$\mathcal{O}$ and $\mathcal{O}_{i}$ be obtained by applying the first $i$
normalization rules to $\mathcal{O}$ (so that $\mathcal{O}_{i+1}$ is obtained
by applying a normalization rule $\mathsf{NF}$ to $\mathcal{O}_{i}$). Assume
that $\mathcal{O}_{i+1}\models(\alpha,m)$. Since the normalization rules can
only introduce new concept names, the concept names occurring in $\mathcal{O}$
are a subset of those occurring in $\mathcal{O}_{i}$, so every concept name
occurring in $\alpha$ occurs in $\mathcal{O}_{i}$. Since we have that
$\mathcal{O}_{i+1}\models(\alpha,m)$, that $\mathcal{O}_{i+1}$ results from
the application of a single normalization rule to $\mathcal{O}_{i}$, and that
all concept names in $\alpha$ occur in $\mathcal{O}_{i}$, the base case
applies and we obtain that $\mathcal{O}_{i}\models(\alpha,m)$. Hence by the
induction hypothesis, $\mathcal{O}\models(\alpha,m)$. ∎

##### Rules for the construction of the canonical model

We will often use the canonical model of the ontology. For convenience, we
recall in Figure 2 its construction in more details for the case where
$\mathcal{O}$ is a satisfiable $\sf{Why}[{\sf X}]$-annotated ontology in
_normal form_.

$\mathcal{I}_{\mathcal{O}}=\bigcup_{i\geq 0}\mathcal{I}_{i}$ where
$\Delta^{\mathcal{I}_{0}}={\sf N_{I}}$, $a^{\mathcal{I}_{0}}=a$ for every
$a\in{\sf N_{I}}$, $A^{\mathcal{I}_{0}}=\\{(a,n)\mid(A(a),n)\in\mathcal{O}\\}$
for every $A\in{\sf N_{C}}$ and
$R^{\mathcal{I}_{0}}=\\{(a,b,n)\mid(R(a,b),n)\in\mathcal{O}\\}$ for every
$R\in{\sf N_{R}}$, and $\mathcal{I}_{i+1}$ results from applying one of the
following rules to $\mathcal{I}_{i}$.

  1. $\mathsf{R}_{1}$

If $(R\sqsubseteq S,n)\in\mathcal{O}$ or $(R^{-}\sqsubseteq
S^{-},n)\in\mathcal{O}$ and $(d,e,o)\in R^{\mathcal{I}_{i}}$, then
$S^{\mathcal{I}_{i+1}}=S^{\mathcal{I}_{i}}\cup\\{(d,e,{o\times n})\\}$.

  2. $\mathsf{R}_{2}$

If $(R\sqsubseteq S^{-},n)\in\mathcal{O}$ or $(R^{-}\sqsubseteq
S,n)\in\mathcal{O}$ and $(d,e,o)\in R^{\mathcal{I}_{i}}$, then
$S^{\mathcal{I}_{i+1}}=S^{\mathcal{I}_{i}}\cup\\{(e,d,{o\times n})\\}$.

  3. $\mathsf{R}_{3}$

If $(A_{1}\sqcap A_{2}\sqsubseteq B,n)\in\mathcal{O}$, $(d,o_{1})\in
A_{1}^{\mathcal{I}_{i}}$ and $(d,o_{2})\in A_{2}^{\mathcal{I}_{i}}$, then
$B^{\mathcal{I}_{i+1}}=B^{\mathcal{I}_{i}}\cup\\{(d,{o_{1}\times o_{2}\times
n})\\}$.

  4. $\mathsf{R}_{4}$

If $(\exists R.A\sqsubseteq B,n)\in\mathcal{O}$, $(d,e,o)\in
R^{\mathcal{I}_{i}}$ and $(e,o^{\prime})\in A^{\mathcal{I}_{i}}$, then
$B^{\mathcal{I}_{i+1}}=B^{\mathcal{I}_{i}}\cup\\{(d,{o\times o^{\prime}\times
n})\\}$.

  5. $\mathsf{R}_{5}$

If $(\exists R^{-}.A\sqsubseteq B,n)\in\mathcal{O}$, $(d,e,o)\in
R^{\mathcal{I}_{i}}$ and $(d,o^{\prime})\in A^{\mathcal{I}_{i}}$, then
$B^{\mathcal{I}_{i+1}}=B^{\mathcal{I}_{i}}\cup\\{(e,{o\times o^{\prime}\times
n})\\}$.

  6. $\mathsf{R}_{6}$

If $(A\sqsubseteq\exists R,n)\in\mathcal{O}$ and $(d,o)\in
A^{\mathcal{I}_{i}}$, then
$\Delta^{\mathcal{I}_{i+1}}=\Delta^{\mathcal{I}_{i}}\cup\\{x\\}$ and
$R^{\mathcal{I}_{i+1}}=R^{\mathcal{I}_{i}}\cup\\{(d,x,{o\times n})\\}$ where
$x\notin\Delta^{\mathcal{I}_{i}}$ is a fresh domain element.

  7. $\mathsf{R}_{7}$

If $(A\sqsubseteq\exists R^{-},n)\in\mathcal{O}$ and $(d,o)\in
A^{\mathcal{I}_{i}}$, then
$\Delta^{\mathcal{I}_{i+1}}=\Delta^{\mathcal{I}_{i}}\cup\\{x\\}$ and
$R^{\mathcal{I}_{i+1}}=R^{\mathcal{I}_{i}}\cup\\{(x,d,{o\times n})\\}$ where
$x\notin\Delta^{\mathcal{I}_{i}}$ is a fresh domain element.

Figure 2: Construction of the canonical model of a satisfiable $\sf{Why}[{\sf
X}]$-annotated ${\cal E\\!LHI}_{\bot}$ ontology in normal form.
$A,A_{1},A_{2}\in{\sf N_{C}}\cup\\{\top\\}$, $B\in{\sf N_{C}}$, and
$R,S\in{\sf N_{R}}$ (recall that RIs and GCIs of $\mathcal{O}$ are of these
forms, except negative RIs and GCIs with $\bot$ as right-hand side, which are
not needed since $\mathcal{O}$ is satisfiable).

##### Proof of Theorem 4.5

We now proceed to prove Theorem 4.5 by showing that $\sf{Why}[{\sf
X}]$-annotated GCI and RI entailments and $\sf{Why}[{\sf X}]$-annotated
assertion entailments can be reduced to each other in polynomial time. When
$\mathcal{O}$ is inconsistent, $\mathcal{O}$ trivially entails every annotated
axiom. We thus focus on proving the case where $\mathcal{O}$ is _satisfiable_.
To increase readability, we divide the proof in several cases, and use the
following lemmas.

Note that Lemmas B.1 and B.2 consider entailment of GCIs that are not part of
the language ${\cal E\\!LHI}_{\bot}$ we consider (since they do not respect
the syntactic restrictions on the right-hand side of the GCI) but whose
semantics is nevertheless well-defined.

######  Lemma B.1.

Let $\mathcal{O}$ be a $\sf{Why}[{\sf X}]$-annotated ${\cal E\\!LHI}_{\bot}$
ontology. Let $C$, $C_{1}$, $C_{2}$, $D_{1}$, $D_{2}$, $D$, $D^{\prime}$ and
$P,P_{1},P_{2}$ be ${\cal E\\!LHI}$ concepts and roles (built according to the
grammar rules $C:=A\mid\exists P.C\mid C\sqcap C\mid\top$, $P:=R\mid R^{-}$,
$A\in{\sf N_{C}}$, $R\in{\sf N_{R}}$). Finally, let $m,m_{1},m_{2}$ be
monomials over ${\sf X}$.

  1. 1.

If $\mathcal{O}\models(C\sqsubseteq C_{1}\sqcap C_{2},m)$,
$\mathcal{O}\models(C_{1}\sqsubseteq D_{1},m_{1})$ and
$\mathcal{O}\models(C_{2}\sqsubseteq D_{2},m_{2})$, then
$\mathcal{O}\models(C\sqsubseteq D_{1}\sqcap D_{2},m\times m_{1}\times
m_{2})$.

  2. 2.

If $\mathcal{O}\models(C\sqsubseteq\exists P_{1}.D^{\prime},m)$,
$\mathcal{O}\models(P_{1}\sqsubseteq P_{2},m_{1})$ and
$\mathcal{O}\models(D^{\prime}\sqsubseteq D,m_{2})$, then
$\mathcal{O}\models(C\sqsubseteq\exists P_{2}.D,m\times m_{1}\times m_{2})$.

###### Proof.

(1) Let $\mathcal{I}$ be a model of $\mathcal{O}$ and $(e,n)\in
C^{\mathcal{I}}$. Since $\mathcal{I}\models(C\sqsubseteq C_{1}\sqcap C_{2},m)$
then $(e,n\times m)\in(C_{1}\sqcap C_{2})^{\mathcal{I}}$ so there exists
$o_{1},o_{2}\in\sf{Why}[{\sf X}]$ such that $(e,o_{1})\in
C_{1}^{\mathcal{I}}$, $(e,o_{2})\in C_{2}^{\mathcal{I}}$, and $o_{1}\times
o_{2}=n\times m$. Hence, since $\mathcal{I}\models(C_{1}\sqsubseteq
D_{1},m_{1})$ and $\mathcal{I}\models(C_{2}\sqsubseteq D_{2},m_{2})$, it holds
that $(e,o_{1}\times m_{1})\in D_{1}^{\mathcal{I}}$ and $(e,o_{2}\times
m_{2})\in D_{2}^{\mathcal{I}}$. It follows that $(e,o_{1}\times m_{1}\times
o_{2}\times m_{2})\in(D_{1}\sqcap D_{2})^{\mathcal{I}}$, i.e. $(e,n\times
m\times m_{1}\times m_{2})\in(D_{1}\sqcap D_{2})^{\mathcal{I}}$. Thus
$\mathcal{O}\models(C\sqsubseteq D_{1}\sqcap D_{2},m\times m_{1}\times
m_{2})$.

(2) Let $\mathcal{I}$ be a model of $\mathcal{O}$ and $(e,n)\in
C^{\mathcal{I}}$. Since $\mathcal{I}\models(C\sqsubseteq\exists
P_{1}.D^{\prime},m)$ then $(e,n\times m)\in(\exists
P_{1}.D^{\prime})^{\mathcal{I}}$ so there exists $f\in\Delta^{\mathcal{I}}$
and $o_{1},o_{2}\in\sf{Why}[{\sf X}]$ such that $(e,f,o_{1})\in
P_{1}^{\mathcal{I}}$, $(f,o_{2})\in{D^{\prime}}^{\mathcal{I}}$, and
$o_{1}\times o_{2}=n\times m$. Hence, since
$\mathcal{I}\models(P_{1}\sqsubseteq P_{2},m_{1})$ and
$\mathcal{O}\models(D^{\prime}\sqsubseteq D,m_{2})$, it holds that
$(e,f,o_{1}\times m_{1})\in P_{2}^{\mathcal{I}}$ and $(f,o_{2}\times
m_{2})\in{D}^{\mathcal{I}}$. It follows that $(e,o_{1}\times m_{1}\times
o_{2}\times m_{2})\in(\exists P_{2}.D)^{\mathcal{I}}$, i.e. $(e,n\times
m\times m_{1}\times m_{2})\in(\exists P_{2}.D)^{\mathcal{I}}$. Thus
$\mathcal{O}\models(C\sqsubseteq\exists P_{2}.D,m\times m_{1}\times m_{2})$. ∎

######  Lemma B.2.

Let $C$ be an ${\cal E\\!LHI}$ concept (built according to the grammar rules
$C:=A\mid\exists P.C\mid C\sqcap C\mid\top$, $P:=R\mid R^{-}$, $A\in{\sf
N_{C}}$, $R\in{\sf N_{R}}$) and $\mathcal{I}_{i}$ be an interpretation. If
$\mathcal{I}_{i+1}$ is an interpretation obtained by applying a rule from
$\\{\mathsf{R}_{1},\mathsf{R}_{2},\mathsf{R}_{3},\mathsf{R}_{4},\mathsf{R}_{5},\mathsf{R}_{6},\mathsf{R}_{7}\\}$
from Figure 2 to $\mathcal{I}_{i}$, and $(d,m)\in C^{\mathcal{I}_{i+1}}$ while
$(d,m)\notin C^{\mathcal{I}_{i}}$, then there exists an ${\cal E\\!LHI}$
concept $D$, $v\in{\sf X}$ and $n\in\sf{Why}[{\sf X}]$ such that
$\mathcal{O}\models(D\sqsubseteq C,v)$, $(d,n)\in D^{\mathcal{I}_{i}}$, and
${v\times n}=m$.

###### Proof.

We prove a stronger version of the property, requiring that $v$ is the
annotation of the GCI or RI of the rule applied to obtain $\mathcal{I}_{i+1}$.
The proof is by structural induction.

_Base case:_ $C\in{\sf N_{C}}$. The rule applied is necessarily
$\mathsf{R}_{3}$, $\mathsf{R}_{4}$ or $\mathsf{R}_{5}$ and since it adds
$(d,m)$ in $C^{\mathcal{I}_{i+1}}$, there exist $(D\sqsubseteq
C,v)\in\mathcal{O}$ (where the form of $D$ depends on the rule used) and
$(d,n)\in D^{\mathcal{I}_{i}}$ such that ${v\times n}=m$. Note that the case
$C=\top$ is not possible since $\top^{\mathcal{I}_{i+1}}$ remains unchanged by
every rule application.

_Induction step._

If $C=C_{1}\sqcap C_{2}$, since $(d,m)\in C^{\mathcal{I}_{i+1}}$, then there
exist $(d,m_{1})\in C_{1}^{\mathcal{I}_{i+1}}$ and $(d,m_{2})\in
C_{2}^{\mathcal{I}_{i+1}}$ such that ${m_{1}\times m_{2}}=m$. Since
$(d,m)\notin C^{\mathcal{I}_{i}}$, then either $(d,m_{1})\notin
C_{1}^{\mathcal{I}_{i}}$ or $(d,m_{2})\notin C_{2}^{\mathcal{I}_{i}}$. Let $v$
be the annotation of the GCI or RI of the rule applied to obtain
$\mathcal{I}_{i+1}$. By induction, we obtain the following.

  * •

If $(d,m_{1})\notin C_{1}^{\mathcal{I}_{i}}$, there exists an ${\cal E\\!LHI}$
concept $D_{1}$ and $n_{1}\in\sf{Why}[{\sf X}]$ such that
$\mathcal{O}\models(D_{1}\sqsubseteq C_{1},v)$, $(d,n_{1})\in
D_{1}^{\mathcal{I}_{i}}$, and ${v\times n_{1}}=m_{1}$.

  * •

If $(d,m_{2})\notin C_{2}^{\mathcal{I}_{i}}$, there exists an ${\cal E\\!LHI}$
concept $D_{2}$ and $n_{2}\in\sf{Why}[{\sf X}]$ such that
$\mathcal{O}\models(D_{2}\sqsubseteq C_{2},v)$, $(d,n_{2})\in
D_{2}^{\mathcal{I}_{i}}$, and ${v\times n_{2}}=m_{2}$.

We thus have three possible cases.

  * •

In the case $(d,m_{1})\notin C_{1}^{\mathcal{I}_{i}}$ and $(d,m_{2})\in
C_{2}^{\mathcal{I}_{i}}$, it holds that $(d,{n_{1}\times
m_{2}})\in(D_{1}\sqcap C_{2})^{\mathcal{I}_{i}}$ and
$\mathcal{O}\models(D_{1}\sqsubseteq C_{1},v)$. Since it trivially holds that
$\mathcal{O}\models(C_{2}\sqsubseteq C_{2},1)$ and
$\mathcal{O}\models(D_{1}\sqcap C_{2}\sqsubseteq D_{1}\sqcap C_{2},1)$, it
follows by Lemma B.1 that $\mathcal{O}\models(D_{1}\sqcap C_{2}\sqsubseteq
C_{1}\sqcap C_{2},v)$ so that $(d,{v\times n_{1}\times m_{2}})\in(C_{1}\sqcap
C_{2})^{\mathcal{I}_{i}}$. Finally, ${v\times n_{1}\times m_{2}}={m_{1}\times
m_{2}}=m$.

  * •

The case $(d,m_{1})\in C_{1}^{\mathcal{I}_{i}}$ and $(d,m_{2})\notin
C_{2}^{\mathcal{I}_{i}}$ is analogous.

  * •

In the case $(d,m_{1})\notin C_{1}^{\mathcal{I}_{i}}$ and $(d,m_{2})\notin
C_{2}^{\mathcal{I}_{i}}$, it holds that $(d,{n_{1}\times
n_{2}})\in(D_{1}\sqcap D_{2})^{\mathcal{I}_{i}}$,
$\mathcal{O}\models(D_{1}\sqsubseteq C_{1},v)$ and
$\mathcal{O}\models(D_{2}\sqsubseteq C_{2},v)$. Since it trivially holds that
$\mathcal{O}\models(D_{1}\sqcap D_{2}\sqsubseteq D_{1}\sqcap D_{2},1)$, it
follows by Lemma B.1 that $\mathcal{O}\models(D_{1}\sqcap D_{2}\sqsubseteq
C_{1}\sqcap C_{2},v)$ so that $(d,{v\times n_{1}\times n_{2}})\in(C_{1}\sqcap
C_{2})^{\mathcal{I}_{i}}$. Finally, ${v\times n_{1}\times n_{2}}={v\times
n_{1}\times v\times n_{2}}={m_{1}\times m_{2}}=m$.

If $C=\exists P.C^{\prime}$, since $(d,m)\in C^{\mathcal{I}_{i+1}}$, then
there exist $(d,f,m_{1})\in P^{\mathcal{I}_{i+1}}$ and
$(f,m_{2})\in{C^{\prime}}^{\mathcal{I}_{i+1}}$ such that ${m_{1}\times
m_{2}}=m$. Since $(d,m)\notin C^{\mathcal{I}_{i}}$, then either
$(d,f,m_{1})\notin P^{\mathcal{I}_{i}}$ or
$(f,m_{2})\notin{C^{\prime}}^{\mathcal{I}_{i}}$. Let $v$ be the annotation of
the GCI or RI of the rule applied to obtain $\mathcal{I}_{i+1}$. We have three
possible cases.

  * •

In the case $(d,f,m_{1})\notin P^{\mathcal{I}_{i}}$ and
$(f,m_{2})\in{C^{\prime}}^{\mathcal{I}_{i}}$, we have two subcases, depending
on the rule that has been applied.

    * $\mathsf{R}_{1}$ or $\mathsf{R}_{2}$:

There exist $(P^{\prime}\sqsubseteq P,v)\in\mathcal{O}$ and $(d,f,n_{1})\in
P^{\prime\mathcal{I}_{i}}$ such that ${v\times n_{1}}=m_{1}$. In this case,
$(d,{n_{1}\times m_{2}})\in(\exists P^{\prime}.C^{\prime})^{\mathcal{I}_{i}}$.
Moreover, since $\mathcal{O}\models(P^{\prime}\sqsubseteq P,v)$ and
$\mathcal{O}\models(C^{\prime}\sqsubseteq C^{\prime},1)$,
$\mathcal{O}\models(\exists P^{\prime}.C^{\prime}\sqsubseteq\exists
P^{\prime}.C^{\prime},1)$, it follows by Lemma B.1 that
$\mathcal{O}\models(\exists P^{\prime}.C^{\prime}\sqsubseteq\exists
P.C^{\prime},v)$ so that $(d,{v\times n_{1}\times m_{2}})\in(\exists
P.C^{\prime})^{\mathcal{I}_{i}}$. Finally, ${v\times n_{1}\times
m_{2}}={m_{1}\times m_{2}}=m$.

    * $\mathsf{R}_{6}$ or $\mathsf{R}_{7}$:

There exist $(A\sqsubseteq\exists P,v)\in\mathcal{O}$ and $(d,n_{1})\in
A^{\mathcal{I}_{i}}$ such that ${v\times n_{1}}=m_{1}$. Moreover, in this case
$f\notin\Delta^{\mathcal{I}_{i}}$ and occurs only in $(d,f,m_{1})\in
P^{\mathcal{I}_{i+1}}$ in $\mathcal{I}_{i+1}$, which implies that
$C^{\prime}=\top$ and $m_{2}=1$, so that $C=\exists P.\top$ and ${m_{1}}=m$,
i.e. ${v\times n_{1}}=m$.

  * •

In the case $(d,f,m_{1})\in P^{\mathcal{I}_{i}}$ and
$(f,m_{2})\notin{C^{\prime}}^{\mathcal{I}_{i}}$, by induction there exists an
${\cal E\\!LHI}$ concept $D$ and $n_{2}\in\sf{Why}[{\sf X}]$ such that
$\mathcal{O}\models(D\sqsubseteq C^{\prime},v)$, $(f,n_{2})\in
D^{\mathcal{I}_{i}}$, and ${v\times n_{2}}=m_{2}$. It follows that
$(d,{m_{1}\times n_{2}})\in{\exists P.D}^{\mathcal{I}_{i}}$. Moreover, since
$\mathcal{O}\models(D\sqsubseteq C^{\prime},v)$,
$\mathcal{O}\models(P\sqsubseteq P,1)$ and $\mathcal{O}\models(\exists
P.D\sqsubseteq\exists P.D,1)$, by Lemma B.1, $\mathcal{O}\models(\exists
P.D\sqsubseteq\exists P.C^{\prime},v)$. Finally, ${v\times m_{1}\times
n_{2}}={m_{1}\times m_{2}}=m$.

  * •

In the case $(d,f,m_{1})\notin P^{\mathcal{I}_{i}}$ and
$(f,m_{2})\notin{C^{\prime}}^{\mathcal{I}_{i}}$, we again have two subcases,
depending on the rule that has been applied (note that in both cases,
$C^{\prime}$ will involve $\exists\mathsf{inv}(P)$).

    * $\mathsf{R}_{1}$ or $\mathsf{R}_{2}$:

There exist $(P^{\prime}\sqsubseteq P,v)\in\mathcal{O}$ and $(d,f,n_{1})\in
P^{\prime\mathcal{I}_{i}}$ such that ${v\times n_{1}}=m_{1}$ and by induction
there exists an ${\cal E\\!LHI}$ concept $D$ and $n_{2}\in\sf{Why}[{\sf X}]$
such that $\mathcal{O}\models(D\sqsubseteq C^{\prime},v)$, $(f,n_{2})\in
D^{\mathcal{I}_{i}}$, and ${v\times n_{2}}=m_{2}$. In this case,
$(d,{n_{1}\times n_{2}})\in(\exists P^{\prime}.D)^{\mathcal{I}_{i}}$.
Moreover, since $\mathcal{O}\models(P^{\prime}\sqsubseteq P,v)$,
$\mathcal{O}\models(D\sqsubseteq C^{\prime},v)$, and
$\mathcal{O}\models(\exists P^{\prime}.D\sqsubseteq\exists P^{\prime}.D,1)$,
it follows by Lemma B.1 that $\mathcal{O}\models(\exists
P^{\prime}.D\sqsubseteq\exists P.C^{\prime},v)$ so that $(d,{v\times
n_{1}\times n_{2}})\in(\exists P.C^{\prime})^{\mathcal{I}_{i}}$. Finally,
${v\times n_{1}\times n_{2}}={v\times n_{1}\times v\times n_{2}}={m_{1}\times
m_{2}}=m$.

    * $\mathsf{R}_{6}$ or $\mathsf{R}_{7}$:

There exist $(A\sqsubseteq\exists P,v)\in\mathcal{O}$ and $(d,n_{1})\in
A^{\mathcal{I}_{i}}$ such that ${v\times n_{1}}=m_{1}$. Moreover, in this case
$f\notin\Delta^{\mathcal{I}_{i}}$ and occurs only in $(d,f,m_{1})\in
P^{\mathcal{I}_{i+1}}$ in $\mathcal{I}_{i+1}$, which implies that
$C^{\prime}=\exists\mathsf{inv}(P).\top$ and $m_{2}=m_{1}$. Hence $C=\exists
P.\exists\mathsf{inv}(P).\top$, and since for every model $\mathcal{I}$ of
$\mathcal{O}$, $(\exists P)^{\mathcal{I}}=(\exists
P.\exists\mathsf{inv}(P).\top)^{\mathcal{I}}=\\{a\mid(a,b,o)\in
P^{\mathcal{I}}\\}$ because $\times$ is idempotent, it follows that
$\mathcal{O}\models(A\sqsubseteq C,v)$. Finally, ${m_{1}}=m_{1}\times
m_{2}=m$, i.e. ${v\times n_{1}}=m$.

This concludes the proof of the lemma. ∎

Let $\mathcal{O}$ be a consistent $\sf{Why}[{\sf X}]$-annotated ${\cal
E\\!LHI}_{\bot}$ ontology in normal form, $C\sqsubseteq D$ be an ${\cal
E\\!LHI}_{\bot}$ GCI, and $m_{0}$ be a monomial over ${\sf X}$. Let
$\mathcal{T}_{D}=\emptyset$ if $D=\bot$, and $\mathcal{T}_{D}=\\{(D\sqsubseteq
E,1)\\}$ otherwise, where $E$ is a concept name that does not occur in
$\mathcal{O}$. Let $\mathcal{A}_{C}=f(C,a_{0},0)$ where $a_{0}$ is an
individual name that does not occur in $\mathcal{O}$ and $f$ is the function
inductively defined as follows, where all constants introduced are fresh, as
well as provenance variables of the form $v^{i}_{A(a)}$ or $v^{i}_{R(a,b)}$:

  * •

$f(\top,a,i)=\emptyset$,

  * •

$f(A,a,i)=\\{(A(a),v^{i}_{A(a)})\\}$ if $A\in{\sf N_{C}}$,

  * •

$f(\exists R.B,a,i)=\\{(R(a,b),v^{i}_{R(a,b)})\\}\cup f(B,b,i+1)$,

  * •

$f(\exists R^{-}.B,a,i)=\\{(R(b,a),v^{i}_{R(b,a)})\\}\cup f(B,b,i+1)$,

  * •

$f(B\sqcap B^{\prime},a,i)=f(B,a,i)\cup f(B^{\prime},a,i+1)$.

Both $\mathcal{T}_{D}$ and $\mathcal{A}_{C}$ can be constructed in polynomial
time.

######  Proposition B.3.

$\mathcal{O}\models(C\sqsubseteq D,m_{0})$ iff
$\mathcal{O}\cup\mathcal{T}_{D}\cup\mathcal{A}_{C}\models(E(a_{0}),m_{0}\times\Pi_{(\alpha,v^{i}_{\alpha})\in\mathcal{A}_{C}}v^{i}_{\alpha})$.

###### Proof.

We start with the case where $D=\bot$.

$(\Rightarrow)$ Assume that $\mathcal{O}\models(C\sqsubseteq\bot,m_{0})$.
Every model $\mathcal{I}$ of
$\mathcal{O}\cup\mathcal{T}_{D}\cup\mathcal{A}_{C}=\mathcal{O}\cup\mathcal{A}_{C}$
should be such that $C^{\mathcal{I}}=\emptyset$ but also such that
$(a_{0}^{\mathcal{I}},\Pi_{(\alpha,v^{i}_{\alpha})\in\mathcal{A}_{C}}v^{i}_{\alpha})\in
C^{\mathcal{I}}$ by construction of $\mathcal{A}_{C}$. Hence
$\mathcal{O}\cup\mathcal{T}_{D}\cup\mathcal{A}_{C}$ is inconsistent. It
follows that
$\mathcal{O}\cup\mathcal{T}_{D}\cup\mathcal{A}_{C}\models(E(a_{0}),m_{0}\times\Pi_{(\alpha,v^{i}_{\alpha})\in\mathcal{A}_{C}}v^{i}_{\alpha})$.

$(\Leftarrow)$ Assume that $\mathcal{O}\not\models(C\sqsubseteq\bot,m_{0})$.
Since $E$ does not occur in
$\mathcal{O}\cup\mathcal{T}_{D}\cup\mathcal{A}_{C}=\mathcal{O}\cup\mathcal{A}_{C}$,
it is easy to check that
$\mathcal{O}\cup\mathcal{T}_{D}\cup\mathcal{A}_{C}\not\models(E(a_{0}),m_{0}\times\Pi_{(\alpha,v^{i}_{\alpha})\in\mathcal{A}_{C}}v^{i}_{\alpha})$.

In the following, we assume that $D\neq\bot$.

$(\Rightarrow)$ Assume that $\mathcal{O}\models(C\sqsubseteq D,m_{0})$ and let
$\mathcal{I}$ be a model of
$\mathcal{O}\cup\mathcal{T}_{D}\cup\mathcal{A}_{C}$. Since
$\mathcal{I}\models\mathcal{O}$, then $\mathcal{I}\models(C\sqsubseteq
D,m_{0})$. Thus, since $\mathcal{I}\models(D\sqsubseteq E,1)$, then
$\mathcal{I}\models(C\sqsubseteq E,m_{0})$. Moreover,
$(a_{0}^{\mathcal{I}},\Pi_{(\alpha,v^{i}_{\alpha})\in\mathcal{A}_{C}}v^{i}_{\alpha})\in
C^{\mathcal{I}}$ by construction of $\mathcal{A}_{C}$, so
$\mathcal{I}\models(E(a_{0}),m_{0}\times\Pi_{(\alpha,v^{i}_{\alpha})\in\mathcal{A}_{C}}v^{i}_{\alpha})$.
Hence
$\mathcal{O}\cup\mathcal{T}_{D}\cup\mathcal{A}_{C}\models(E(a_{0}),m_{0}\times\Pi_{(\alpha,v^{i}_{\alpha})\in\mathcal{A}_{C}}v^{i}_{\alpha})$.

$(\Leftarrow)$ We show the other direction by contrapositive: We assume that
$\mathcal{O}\not\models(C\sqsubseteq D,m_{0})$ and show that
$\mathcal{O}\cup\mathcal{T}_{D}\cup\mathcal{A}_{C}\not\models(E(a_{0}),m_{0}\times\Pi_{(\alpha,v^{i}_{\alpha})\in\mathcal{A}_{C}}v^{i}_{\alpha})$.
Let $\mathcal{I}=\bigcup_{j\geq 0}\mathcal{I}_{j}$ be the canonical model of
$\mathcal{O}\cup\mathcal{T}_{D}\cup\mathcal{A}_{C}$, obtained starting from
$\mathcal{I}_{0}$ and applying rules $\mathsf{R}_{1},\dots,\mathsf{R}_{7}$
from Figure 2. We show by induction on $j$ that for every $m$ over ${\sf X}$
(hence such that $m$ does not contain any variable of the form
$v^{i}_{\alpha}$) and general ${\cal E\\!LHI}$ concept $G\neq\top$, if
$(a_{0},{m\times\Pi_{(\alpha,v^{i}_{\alpha})\in\mathcal{A}_{C}}v^{i}_{\alpha}})\in
G^{\mathcal{I}_{j}}$ then $\mathcal{O}\models(C\sqsubseteq G,m)$.

_Base case: $j=0$._ If
$(a_{0},{m\times\Pi_{(\alpha,v^{i}_{\alpha})\in\mathcal{A}_{C}}v^{i}_{\alpha}})\in
G^{\mathcal{I}_{0}}$, by construction of $\mathcal{I}_{0}$, we know that
${m\times\Pi_{(\alpha,v^{i}_{\alpha})\in\mathcal{A}_{C}}v^{i}_{\alpha}}={\Pi_{(\alpha,v^{i}_{\alpha})\in\mathcal{A}_{C}}v^{i}_{\alpha}}$
and $m=1$. We show by structural induction on $C$ that for every $a\in{\sf
N_{I}}$, $(a,{\Pi_{(\alpha,v^{i}_{\alpha})\in f(C,a,k)}v^{i}_{\alpha}})\in
G^{\mathcal{I}_{0}}$ implies $\mathcal{O}\models(C\sqsubseteq G,1)$.

  * •

Base case: If $C=A\in{\sf N_{C}}$, $C=\top$, $C=\exists R.\top$, or $C=\exists
R^{-}.\top$, $f(C,a,k)$ is equal to $\\{(A(a),v^{k}_{A(a)})\\}$, $\emptyset$,
$\\{(R(a,b),v^{k}_{R(a,b)})\\}$ or $\\{(R(b,a),v^{k}_{R(b,a)})\\}$
respectively. Hence, $(a,v^{k}_{\alpha})\in G^{\mathcal{I}_{0}}$ implies that
$G$ is equivalent to $C$, so that $\mathcal{O}\models(C\sqsubseteq G,1)$
(since $\times$ is idempotent).

  * •

If $C=C_{1}\sqcap C_{2}$, then $f(C,a,k)=f(C_{1},a,k)\cup f(C_{2},a,k+1)$.
Since $(a,{\Pi_{(\alpha,v^{i}_{\alpha})\in
f(C_{1},a,k)}v^{i}_{\alpha}\times\Pi_{(\alpha,v^{i}_{\alpha})\in
f(C_{2},a,k+1)}v^{i}_{\alpha}})\in G^{\mathcal{I}_{0}}$, $G$ is equivalent to
some $G_{1}\sqcap G_{2}$ with $(a,{\Pi_{(\alpha,v^{i}_{\alpha})\in
f(C_{1},a,k)}v^{i}_{\alpha}})\in G_{1}^{\mathcal{I}_{0}}$ and
$(a,{\Pi_{(\alpha,v^{i}_{\alpha})\in f(C_{2},a,k+1)}v^{i}_{\alpha}})\in
G_{2}^{\mathcal{I}_{0}}$. By induction, $\mathcal{O}\models(C_{1}\sqsubseteq
G_{1},1)$ and $\mathcal{O}\models(C_{2}\sqsubseteq G_{2},1)$. Hence, since it
trivially holds that $\mathcal{O}\models(C\sqsubseteq C_{1}\sqcap C_{2},1)$,
it follows by Lemma B.1 that $\mathcal{O}\models(C\sqsubseteq G,1)$.

  * •

If $C=\exists R.C^{\prime}$, then $f(C,a,k)=\\{(R(a,b),v^{k}_{R(a,b)})\\}\cup
f(C^{\prime},b,k+1)$. Since
$(a,{v^{k}_{R(a,b)}\times\Pi_{(\alpha,v^{i}_{\alpha})\in
f(C^{\prime},b,k+1)}v^{i}_{\alpha}})\in G^{\mathcal{I}_{0}}$, $G$ is
equivalent to some $\exists R.G^{\prime}$ with
$(b,{\Pi_{(\alpha,v^{i}_{\alpha})\in f(C^{\prime},b,k+1)}v^{i}_{\alpha}})\in
G^{\prime\mathcal{I}_{0}}$. By induction,
$\mathcal{O}\models(C^{\prime}\sqsubseteq G^{\prime},1)$. Hence, since it
trivially holds that $\mathcal{O}\models(C\sqsubseteq\exists R.C^{\prime},1)$,
it follows by Lemma B.1 that $\mathcal{O}\models(C\sqsubseteq G,1)$.

  * •

The case $C=\exists R^{-}.C^{\prime}$ is analogous.

This shows the property for $j=0$: if
$(a_{0},{\Pi_{(\alpha,v^{i}_{\alpha})\in\mathcal{A}_{C}}v^{i}_{\alpha}})\in
G^{\mathcal{I}_{0}}$, then $\mathcal{O}\models(C\sqsubseteq G,1)$.

_Inductive step._ Assume that for every monomial $m$ over ${\sf X}$ (hence
without variables of the form $v^{i}_{\alpha}$) and general ${\cal E\\!LHI}$
concept $G\neq\top$, if
$(a_{0},{m\times\Pi_{(\alpha,v^{i}_{\alpha})\in\mathcal{A}_{C}}v^{i}_{\alpha}})\in
G^{\mathcal{I}_{j}}$ then $\mathcal{O}\models(C\sqsubseteq G,m)$. Let $m$ be a
monomial over ${\sf X}$ and $G\neq\top$ and assume that
$(a_{0},{m\times\Pi_{(\alpha,v^{i}_{\alpha})\in\mathcal{A}_{C}}v^{i}_{\alpha}})\in
G^{\mathcal{I}_{j+1}}$. If
$(a_{0},{m\times\Pi_{(\alpha,v^{i}_{\alpha})\in\mathcal{A}_{C}}v^{i}_{\alpha}})\in
G^{\mathcal{I}_{j}}$, then $\mathcal{O}\models(C\sqsubseteq G,m)$ by induction
hypothesis. Otherwise, by Lemma B.2, since $\mathcal{I}_{j+1}$ is obtained by
applying one of the rules $\mathsf{R}_{1},\dots,\mathsf{R}_{7}$ from Figure 2
to $\mathcal{I}_{j}$, and
$(a_{0},{m\times\Pi_{(\alpha,v^{i}_{\alpha})\in\mathcal{A}_{C}}v^{i}_{\alpha}})\in
G^{\mathcal{I}_{j+1}}$ while
$(a_{0},{m\times\Pi_{(\alpha,v^{i}_{\alpha})\in\mathcal{A}_{C}}v^{i}_{\alpha}})\notin
G^{\mathcal{I}_{j}}$, there exists an ${\cal E\\!LHI}$ concept $F$, a
provenance variable $v\in{\sf X}$ and a monomial $n$ such that
$\mathcal{O}\models(F\sqsubseteq G,v)$, $(a_{0},n)\in F^{\mathcal{I}_{j}}$,
and ${v\times
n}={m\times\Pi_{(\alpha,v^{i}_{\alpha})\in\mathcal{A}_{C}}v^{i}_{\alpha}}$.
Recall that the provenance variables of form $v^{i}_{\alpha}$ are not in ${\sf
X}$. There thus exists a monomial $n^{\prime}$ that does not contain any
$v^{i}_{\alpha}$ and is such that
${n}={n^{\prime}\times\Pi_{(\alpha,v^{i}_{\alpha})\in\mathcal{A}_{C}}v^{i}_{\alpha}}$
and ${v\times n^{\prime}}=m$. Since $(a_{0},n)\in F^{\mathcal{I}_{j}}$, it
follows by induction that $\mathcal{O}\models(C\sqsubseteq F,n^{\prime})$.
Hence, since $\mathcal{O}\models(F\sqsubseteq G,v)$, we conclude that
$\mathcal{O}\models(C\sqsubseteq G,v\times n^{\prime})$, i.e. that
$\mathcal{O}\models(C\sqsubseteq G,m)$.

Thus for every ${\cal E\\!LHI}$ concept $G\neq\top$ and monomial $m$ over