# Semiring Provenance for Lightweight Description Logics

Camille Bourgaux<EMAIL_ADDRESS>
DI ENS, ENS, CNRS, PSL University & Inria
45 rue d’Ulm
75230 Paris Cedex 05, France Ana Ozaki<EMAIL_ADDRESS>
University of Oslo
Gaustadalléen 23B
0373, Oslo, Norway Rafael Peñaloza<EMAIL_ADDRESS>
University of Milano-Bicocca
Viale Sarca 336, U14-2054
20126, Milan, Italy

###### Abstract

We investigate semiring provenance—a successful framework originally defined
in the relational database setting—for description logics. In this context,
the ontology axioms are annotated with elements of a commutative semiring and
these annotations are propagated to the ontology consequences in a way that
reflects how they are derived. We define a provenance semantics for a language
that encompasses several lightweight description logics and show its
relationships with semantics that have been defined for ontologies annotated
with a specific kind of annotation (such as fuzzy degrees). We show that under
some restrictions on the semiring, the semantics satisfies desirable
properties (such as extending the semiring provenance defined for databases).
We then focus on the well-known why-provenance, which allows to compute the
semiring provenance for every additively and multiplicatively idempotent
commutative semiring, and for which we study the complexity of problems
related to the provenance of an axiom or a conjunctive query answer. Finally,
we consider two more restricted cases which correspond to the so-called
positive Boolean provenance and lineage in the database setting. For these
cases, we exhibit relationships with well-known notions related to
explanations in description logics and complete our complexity analysis. As a
side contribution, we provide conditions on an ${\cal E\\!LHI}_{\bot}$
ontology that guarantee tractable reasoning.

##  1 Introduction

Description logics (DLs) are a well-known family of first-order logic
fragments in which conceptual knowledge about a particular domain and facts
about specific individuals are expressed in an ontology, using unary and
binary predicates called concepts and roles (?). Important reasoning tasks
performed over DL ontologies are axiom entailment, i.e. deciding whether a
given DL axiom follows from the ontology; and query answering, focussing in
particular in database-style conjunctive queries. Since scalability is crucial
when using large ontologies, DLs with favorable computational properties have
been investigated. In particular, the DL-Lite and ${\cal E\\!L}$ families
propose many dialects that allow for axiom entailment in polynomial time, and
Boolean conjunctive query entailment in NP (?, ?, ?). Many real-world
ontologies use languages from these families, which underly the OWL 2 QL and
OWL 2 EL profiles of the Semantic Web standard ontology language (?). Several
extensions of DLs go beyond simple axiom or query entailment and enrich the
results with additional information. One can mention fuzzy DLs to express
vagueness (?, ?), possibilistic DLs to handle uncertainty (?), or the bag
semantics, which associates multiplicities to query results (?, ?). Another
kind of information that may be expected to accompany reasoning results is
explanation. It may indeed be crucial to know how a consequence—e.g. an axiom
or a query—has been derived from the ontology. Explaining inferences in DLs
has been studied mostly focusing on explaining axiom entailment, in particular
concept subsumption, through axiom pinpointing, which consists in finding
minimal subsets of the ontology that entail the consequence (?, ?, ?). A
similar approach was investigated for explaining ontology-mediated query
answers, but focussing only on the minimal subsets of facts which together
with the conceptual knowledge entail the query (?, ?). Alternative approaches
that consider the whole ontology provide more involved proof-based
explanations (?, ?, ?). Investigation of proofs for axiom entailment that go
beyond axiom pinpoiting is also an active line of research (?, ?).

Within the context of databases, the framework of _semiring provenance_ (?, ?)
generalizes the semantics of queries over annotated databases to allow
algebraic computations over different kinds of annotations, such as
multiplicities, trust levels, costs, clearance levels, etc. In this framework,
the semantics of positive relational algebra queries over databases annotated
with elements of any commutative semiring is inductively defined on the
structure of the query (?, ?). Intuitively, joint use of the data corresponds
to the semiring multiplication while alternative use of the data corresponds
to the semiring addition. This framework captures many notions of provenance
or explanation that have been considered in the database community for nearly
30 years, such as lineage or why-provenance (?, ?), by introducing so called
_provenance semirings_ which abstract from a specific semiring and compute a
representation of the provenance (?). Provenance semirings serve as an
abstract algebraic tool to record and track provenance information; that is,
to keep track of the specific database tuples used for deriving the query, and
of the way they have been processed in the derivation. Provenance semirings
elements are expressions (such as polynomials) built from variables associated
with each tuple of the database. A provenance expression provides a general
representation of how tuples have been used to derive a query result. It can
be faithfully evaluated in any semiring in which the considered provenance
semiring can be homomorphically embedded. Semiring provenance has also been
studied for Datalog queries, for which it is defined based on the set of all
derivation trees for the query (?, ?, ?), and has drawn interest beyond
relational databases, notably in the context of the Semantic Web (?, ?, ?, ?,
?), but also XML (?), graph databases (?, ?), and expressive logics (?, ?). We
refer to Section 6 for more details on provenance related work.

In this work, we investigate semiring provenance for description logic
ontologies. An important feature that distinguishes DL ontologies from the
relational database setting is that not only facts but also axioms expressing
conceptual knowledge can be annotated and, thus, need to be traced. We also
consider not only query answering—as it is done for Datalog queries which can
be seen as ontologies—but also axiom entailment, such as concept subsumption,
which is a classical reasoning task for DL.

There have already been several proposals to use provenance semirings with
description logic ontologies (?, ?, ?, ?) (see Section 6 for a more detailed
discussion). In particular, ? (?) consider ontology-based data access, a
setting where a database is enriched with a DL-LiteR ontology and mappings
between them, and ? (?) consider axiom entailment and query answering in
${\cal E\\!LH}^{r}$. In these two papers, the ontology axioms are annotated
with provenance variables, and consequences of the ontology (axioms or
queries) are annotated with provenance polynomials expressing their provenance
information. However, if these polynomials can be used as explanations, these
papers do not investigate whether the considered semantics captures some of
the existing semantics for annotated ontologies (such as the fuzzy semantics
or the bag semantics). This is indeed not straightforward, as recently shown
by ? (?) who consider several ways of defining semiring provenance for Datalog
and found that the one inspired by the semantics used by ? and ? does not have
this property when used with semirings that do not fulfill some additional
properties. In this paper, we thus revisit and extend this line of research.
We next describe our main contributions.

  * •

In Section 3, we define a semiring provenance semantics for (a syntactic
restriction of) ${\cal E\\!LHI}_{\bot}$, a DL language that encompasses
several dialects of the DL-Lite and ${\cal E\\!L}$ families, discuss its
relationships with semantics defined for specific applications, and
investigate its properties. In particular, we show that our provenance
semantics satisfies some desirable properties when restricted to commutative
semirings that are additively and multiplicatively idempotent and discuss the
problems that arise beyond this setting.

  * •

In Section 4, we focus on additively and multiplicatively idempotent
commutative semirings, which are captured by a provenance semiring that
corresponds to the well-known why-provenance in the database setting. We
provide algorithms and complexity results for computing the provenance of
axioms and queries in this semiring for ${\cal E\\!LHI}_{\bot}$. We also
include in our complexity analysis a fragment of ${\cal E\\!LHI}_{\bot}$ that
encompasses several dialects of the DL-Lite and ${\cal E\\!L}$ families, for
which we show that reasoning is tractable in the standard, non-annotated
setting. This fragment is actually a side contribution of the paper, since it
provides some insights on the complexity of reasoning with ${\cal
E\\!LHI}_{\bot}$ ontologies.

  * •

In Section 5, we consider two cases that add further conditions on the
semiring and correspond to the so-called positive Boolean provenance and
lineage in the database setting. We exhibit relationships with well-known
notions related to explanations in DLs and also provide algorithms and
complexity results for ${\cal E\\!LHI}_{\bot}$ and its restriction.

For the ease of reading, we choose to delegate most of the proofs (which may
be long and technical but mostly rely on classical techniques) to the
appendix.

##  2 Preliminaries

This section recalls the syntax and semantics of description logics and the
framework of semiring provenance in the context of databases.

###  2.1 Description Logics and the ${\cal E\\!LHI}_{\bot}$ Language

Our main focus will be on (a syntactic restriction of) the DL language ${\cal
E\\!LHI}_{\bot}$, which encompasses several dialects of the well-known ${\cal
E\\!L}$ (?) and DL-Lite (?) families of lightweight description logics.

##### Syntax

Let ${\sf N_{C}}$, ${\sf N_{R}}$ and ${\sf N_{I}}$ be three mutually disjoint
countable sets of _concept-_ , _role-_ , and _individual names_ ,
respectively. Given a DL language $\mathcal{L}$, an $\mathcal{L}$ _ontology_
$\mathcal{O}$ is a finite set of _axioms_ whose form depends on $\mathcal{L}$.
We consider the following kinds of axioms.

  * •

Concept and role _assertions_ are of the form $A(a)$ and $R(a,b)$
respectively, with $A\in{\sf N_{C}}$, $R\in{\sf N_{R}}$, and $a,b\in{\sf
N_{I}}$.

  * •

_General concept inclusions_ (GCIs) are expressions of the form $C\sqsubseteq
D$, built according to the grammar rules

$C::=A\mid\exists P.C\mid C\sqcap C\mid\top\quad\quad\quad D::=A\mid\exists
P.\top\mid\bot\quad\quad\quad P::=R\mid R^{-}$

where $R\in{\sf N_{R}}$, $A\in{\sf N_{C}}$. We often use $\exists P$ as a
shorthand for $\exists P.\top$, and we call _basic concepts_ the concepts of
the form $A$ or $\exists P$.

  * •

Positive _role inclusions_ (RIs) are of the form $P\sqsubseteq Q$ with
$P,Q::=R\mid R^{-}$ for $R\in{\sf N_{R}}$ and _negative role inclusions_ are
of the form $P\sqcap Q\sqsubseteq\bot$.

An ${\cal E\\!LHI}_{\bot}$ _ontology_ is a finite set of axioms of any of the
available forms. A _DL-Lite R ontology_ may contain assertions, positive and
negative role inclusions, and GCIs of one of the following restricted forms:
$D_{1}\sqsubseteq D_{2}$ or $D_{1}\sqcap D_{2}\sqsubseteq\bot$ where $D_{1}$
and $D_{2}$ are _basic concepts_. An ${\cal E\\!LH}^{r}$ _ontology_ may
contain all the considered axioms with the restrictions that (i) $\bot$ does
not occur in the ontology and (ii) there is no inverse role (i.e. $P::=R$),
except for _range restrictions_ of the form $\exists R^{-}\sqsubseteq A$.

In the standard DL literature, languages from the ${\cal E\\!L}$ family
usually allow for GCIs of the general form $C\sqsubseteq C$ with $C$
constructed as in the previous grammar rules, but our syntactic restrictions
are made without loss of generality. Indeed, such GCIs can be translated into
our syntax by exhaustively applying the following rules: (i) replace
$C\sqsubseteq C_{1}\sqcap C_{2}$ by $C\sqsubseteq C_{1}$ and $C\sqsubseteq
C_{2}$, (ii) replace $C_{1}\sqsubseteq\exists P.C_{2}$ by
$C_{1}\sqsubseteq\exists S$, $S\sqsubseteq P$ and $\exists S^{-}\sqsubseteq
C_{2}$ where $S$ is a fresh role name. The reason for this syntactic
restriction is that conjunctions or qualified restrictions of a role on the
right-hand side of GCIs lead to counter-intuitive behaviour when dealing with
provenance. We discuss this issue in further detail in Section 3.6.

Given an ontology $\mathcal{O}$, we denote by $\mathsf{sig}(\mathcal{O})$ the
set of concept and role names that occur in $\mathcal{O}$ and by
$\mathsf{ind}(\mathcal{O})$ the set of individual names that occur in
$\mathcal{O}$. Moreover, for $R\in{\sf N_{R}}$, we let $\mathsf{inv}(R)=R^{-}$
and $\mathsf{inv}(R^{-})=R$.

##### Semantics

The semantics of DL languages is defined through _interpretations_ , in the
spirit of first-order logic. An interpretation is a pair
$\mathcal{I}=(\Delta^{\mathcal{I}},\cdot^{\mathcal{I}})$ where
$\Delta^{\mathcal{I}}$ is a non-empty set (called the _domain_ of
$\mathcal{I}$), and $\cdot^{\mathcal{I}}$ is the _interpretation function_ ,
which maps every $a\in{\sf N_{I}}$ to
$a^{\mathcal{I}}\in\Delta^{\mathcal{I}}$; every $A\in{\sf N_{C}}$ to
$A^{\mathcal{I}}\subseteq\Delta^{\mathcal{I}}$; and every $R\in{\sf N_{R}}$ to
$R^{\mathcal{I}}\subseteq\Delta^{\mathcal{I}}\times\Delta^{\mathcal{I}}$.

The interpretation function $\cdot^{\mathcal{I}}$ is extended to complex
expressions as follows:

$\displaystyle(\top)^{\mathcal{I}}={}$ $\displaystyle\Delta^{\mathcal{I}};$
$\displaystyle(\bot)^{\mathcal{I}}={}$ $\displaystyle\emptyset;$
$\displaystyle(R^{-})^{\mathcal{I}}={}$ $\displaystyle\\{(e,d)\mid(d,e)\in
R^{\mathcal{I}}\\};$ $\displaystyle(\exists P.C)^{\mathcal{I}}={}$
$\displaystyle\\{d\mid\exists e\in\Delta^{\mathcal{I}}\text{ s.t. }(d,e)\in
P^{\mathcal{I}},e\in C^{\mathcal{I}}\\};$ $\displaystyle(C\sqcap
D)^{\mathcal{I}}={}$ $\displaystyle C^{\mathcal{I}}\cap D^{\mathcal{I}}.$

The interpretation $\mathcal{I}$ _satisfies_ the concept assertion $A(a)$ if
$a^{\mathcal{I}}\in A^{\mathcal{I}}$; the role assertion $R(a,b)$ if
$(a^{\mathcal{I}},b^{\mathcal{I}})\in R^{\mathcal{I}}$; the GCI $C\sqsubseteq
D$ if $C^{\mathcal{I}}\subseteq D^{\mathcal{I}}$; the positive RI
$P\sqsubseteq Q$ if $P^{\mathcal{I}}\subseteq Q^{\mathcal{I}}$; and the
negative RI $P\sqcap Q\sqsubseteq\bot$ if $P^{\mathcal{I}}\cap
Q^{\mathcal{I}}=\emptyset$. The satisfaction of an axiom $\alpha$ by
$\mathcal{I}$ is denoted $\mathcal{I}\models\alpha$. The interpretation
$\mathcal{I}$ is a _model_ of the ontology $\mathcal{O}$, denoted by
$\mathcal{I}\models\mathcal{O}$, iff $\mathcal{I}\models\alpha$ for every
$\alpha\in\mathcal{O}$. Finally, $\mathcal{O}$ _entails_ an axiom $\alpha$ if
$\mathcal{I}\models\alpha$ for every model $\mathcal{I}$ of $\mathcal{O}$.

##### Queries

A _conjunctive query_ (CQ) is an existentially quantified formula
$\exists\vec{y}\,\phi(\vec{x},\vec{y})$ where $\phi(\vec{x},\vec{y})$ is a
conjunction of atoms of the form $A(t)$ or $R(t,t^{\prime})$ with $A\in{\sf
N_{C}}$, $R\in{\sf N_{R}}$, and terms $t,t^{\prime}\in{\sf
N_{I}}\cup\vec{x}\cup\vec{y}$. We denote by $\mathsf{atoms}(q)$ and
$\mathsf{terms}(q)$ the sets of atoms and terms of a query $q$. A CQ
consisting of a single atom is called an _atomic query_. A _union of
conjunctive queries_ (UCQ) is a disjunction of CQs (over the same free
variables). A query is _Boolean_ if it has no free-variables. An
interpretation $\mathcal{I}$ satisfies a Boolean CQ (BCQ)
$q:=\exists\vec{y}\,\phi(\vec{y})$, written $\mathcal{I}\models q$, iff there
is a _match for $q$ in $\mathcal{I}$_, where a match for $q$ in $\mathcal{I}$
is a function $\pi:\mathsf{terms}(q)\rightarrow\Delta^{\mathcal{I}}$ such that
$\pi(t)=t^{\mathcal{I}}$ for every $t\in{\sf N_{I}}$, $\pi(t)\in
A^{\mathcal{I}}$ for every $A(t)\in\mathsf{atoms}(q)$, and
$(\pi(t),\pi(t^{\prime}))\in R^{\mathcal{I}}$ for every
$R(t,t^{\prime})\in\mathsf{atoms}(q)$. A BCQ $q$ is _entailed_ by an ontology
$\mathcal{O}$, written $\mathcal{O}\models q$, if and only if
$\mathcal{I}\models q$ for every model $\mathcal{I}$ of $\mathcal{O}$. A tuple
of constants $\vec{a}$ is an _answer_ to a CQ
$q(\vec{x}):=\exists\vec{y}\,\phi(\vec{x},\vec{y})$ over $\mathcal{O}$ if
$\vec{a}$ and $\vec{x}$ have the same arity and $\mathcal{O}\models
q(\vec{a})$ where $q(\vec{a})$ is the BCQ obtained by replacing the variables
from $\vec{x}$ with the corresponding constants from $\vec{a}$.

| axiom entailment | BCQ entailment
---|---|---
${\cal E\\!LHI}_{\bot}$ (?) |  ExpTime-complete |  ExpTime-complete
${\cal E\\!L}$ (?, ?) | in PTime |  NP-complete
DL-Lite (?) | in PTime |  NP-complete
$\mathcal{ELHI_{\bot}^{\mathit{restr}}}$ (Theorem 2.2) | in PTime |  NP-complete
Table 1: Combined complexity of axiom and BCQ entailment in different DLs.

##### Complexity

The complexity of axiom entailment and BCQ entailment in the different
languages we consider is summarised in Table 1. We consider only the _combined
complexity_ ; that is, everything—all the axioms in the ontology and the
query—is part of the input and measured accordingly.

##### $\boldsymbol{\mathcal{ELHI_{\bot}^{\mathit{restr}}}}$

To discuss lightweight DLs such as ${\cal E\\!LH}^{r}$ and DL-LiteR, we define
a fragment of ${\cal E\\!LHI}_{\bot}$ which extends them and shares their good
computational properties.

######  Definition 2.1 ($\mathcal{ELHI_{\bot}^{\mathit{restr}}}$).

We say that an ${\cal E\\!LHI}_{\bot}$ ontology $\mathcal{O}$ belongs to
$\mathcal{ELHI_{\bot}^{\mathit{restr}}}$ if

  1. 1.

$\mathcal{O}$ is in _normal form_ , i.e. its GCIs are of the form

$A\sqsubseteq B,\ A\sqcap A^{\prime}\sqsubseteq B,\ A\sqsubseteq\exists R,\
A\sqsubseteq\exists R^{-},\ \exists R.A\sqsubseteq B,\text{ or }\exists
R^{-}.A\sqsubseteq B$

with $A,A^{\prime}\in{\sf N_{C}}\cup\\{\top\\}$, $B\in{\sf
N_{C}}\cup\\{\bot\\}$;

  2. 2.

$\mathcal{O}$ is such that for every role or inverse role $P$, if there exists
$C\in{\sf N_{C}}$ and such that $\mathcal{O}\models C\sqsubseteq\exists P$,
then for every $\exists\mathsf{inv}(P).A\sqsubseteq B\in\mathcal{O}$, it holds
that $A=\top$.

The algorithms we develop in Section 4 will allow us to prove the following
result.

######  Theorem 2.2.

For ontologies that belong to $\mathcal{ELHI_{\bot}^{\mathit{restr}}}$,
satisfiability and axiom entailment are in PTime and BCQ entailment is NP-
complete.

###  2.2 Semiring Provenance in the Database Setting

In the database setting, the framework of _semiring provenance_ generalizes
the semantics of queries over annotated databases. We explain the main notions
of this field next, assuming a basic understanding of relational databases
(?).

##### Queries over annotated databases

In semiring provenance, database facts are annotated with elements of
algebraic structures known as _commutative semirings_. A semiring
$\mathbb{K}=(K,\oplus,\otimes,\mathbb{0},\mathbb{1})$ consists of a set $K$
with distinguished elements $\mathbb{0}$ and $\mathbb{1}$, equipped with two
binary operators: the _addition_ $\oplus$, which is an associative and
commutative operator with identity $\mathbb{0}$, and the _multiplication_
$\otimes$, which is an associative operator with identity $\mathbb{1}$ such
that $\otimes$ distributes over $\oplus$ and $\mathbb{0}$ is annihilating for
$\otimes$. A semiring is called _commutative_ when $\otimes$ is commutative.
We use the convention according to which multiplication has precedence over
addition to omit parentheses (i.e. $a\oplus b\otimes c$ is $a\oplus(b\otimes
c)$).

A semiring is _$\oplus$ -idempotent_ (resp. _$\otimes$ -idempotent_) if for
every $a\in K$, $a\oplus a=a$ (resp. $a\otimes a=a$). It is _absorptive_ if
for every $a,b\in K$, $a\otimes b\oplus a=a$. Note that if a semiring is
absorptive, then it is also $\oplus$-idempotent (since $a\oplus
a=a\otimes\mathbb{1}\oplus a=a$). Finally, a semiring is _positive_ if for
every $a,b\in K$, (i) $a\otimes b=0$ iff $a=0$ or $b=0$, and (ii) $a\oplus
b=0$ iff $a=b=0$.

######  Example 2.3.

We consider the following commutative semirings in our running example.

  * •

The counting semiring $\mathbb{N}=(\mathbb{N},+,\times,0,1)$ is the set of the
natural integers equipped with the usual addition and multiplication between
integers.

  * •

The tropical semiring $\mathbb{T}=(\mathbb{R}^{\infty}_{+},\min,+,\infty,0)$,
used to represent costs, is the set of positive real numbers extended with the
symbol $\infty$, with the minimum operation as addition ($a\oplus
b=\min(a,b)$) and standard addition as multiplication ($a\otimes b=a+b$).

  * •

The Viterbi semiring $\mathbb{V}=([0,1],\max,\times,0,1)$, used to represent
confidence scores, is the set of real numbers between $0$ and $1$ with the
maximum operation as addition ($a\oplus b=\max(a,b)$) and the usual
multiplication between reals ($a\otimes b=a\times b$).

  * •

The fuzzy semiring $\mathbb{F}=([0,1],\max,\min,0,1)$, used to represent truth
degrees, is the set of real numbers between $0$ and $1$ with the maximum
operation as addition ($a\oplus b=\max(a,b)$) and the minimum operation as
multiplication ($a\otimes b=\min(a,b)$).

  * •

The Łukasiewicz semiring $\mathbb{L}=([0,1],\max,\star_{L},0,1)$, used to
represent truth values, is the set of real numbers between $0$ and $1$ with
the maximum operation as addition ($a\oplus b=\max(a,b)$) and multiplication
defined by $a\star_{L}b=\max(0,a+b-1)$.

  * •

The access control semiring $\mathbb{A}=(\\{P<C<S<T<0\\},\min,\max,0,P)$, used
to represent clearance levels required to access data (?), is the set
$\\{P,C,S,T,0\\}$ (for “public”, “confidential”, “secret”, “top-secret”, and
“nobody knows”) with the minimum and maximum operations w.r.t. the obvious
total ordering $P<C<S<T<0$ as addition and multiplication respectively. More
generally, ? (?) define clearance levels through a distributive lattice
$(L,\min,\max,\bot,\top)$, which allows for incomparable levels and a higher
level of granularity.

From these examples, the counting semiring is the only one which is not
absorptive nor $\oplus$-idempotent; the fuzzy and the access control semirings
are the only ones which are $\otimes$-idempotent; and the Łukasiewicz semiring
is the only one that is not positive since, for example,
$0.1\star_{L}0.1=\max(0,0.1+0.1-1)=0$. ∎

The semantics of positive relational algebra queries over databases annotated
with elements of any commutative semiring is defined inductively on the
structure of the query (?, ?). Intuitively, joint use of the data corresponds
to the semiring multiplication while alternative use of the data corresponds
to the semiring addition. In other words, we _multiply_ the annotations of all
the facts that together produce an answer, and _add_ such products over all
combinations yielding the same answer.

######  Example 2.4.

Consider the three facts $\mathsf{Deity}(\mathsf{Dionysus})$,
$\mathsf{mother}(\mathsf{Dionysus},\mathsf{Semele})$ and
$\mathsf{mother}(\mathsf{Dionysus},\mathsf{Demeter})$, stating that Dionysus
is a deity which has mother Semele and Demeter, and the query $\exists
xy\,\mathsf{Deity}(x)\wedge\mathsf{mother}(x,y)$ that asks if there is a deity
which has a mother. The answer is _yes_ and it can be derived either using
$\mathsf{Deity}(\mathsf{Dionysus})$ and
$\mathsf{mother}(\mathsf{Dionysus},\mathsf{Semele})$ or using
$\mathsf{Deity}(\mathsf{Dionysus})$ and
$\mathsf{mother}(\mathsf{Dionysus},\mathsf{Demeter})$, interpreting $y$ by
either $\mathsf{Semele}$ or $\mathsf{Demeter}$. We now annotate the facts
$\mathsf{Deity}(\mathsf{Dionysus})$,
$\mathsf{mother}(\mathsf{Dionysus},\mathsf{Semele})$ and
$\mathsf{mother}(\mathsf{Dionysus},\mathsf{Demeter})$ with elements of the
semirings introduced in Example 2.3.

  * •

Assume that the facts are annotated with multiplicities $3$, $2$ and $1$
respectively, from $\mathbb{N}=(\mathbb{N},+,\times,0,1)$. The multiplicity of
the query is $3\times 2+3\times 1=9$.

  * •

Assume that the facts are annotated with costs to pay to access them $1$, $5$
and $8$ respectively, from
$\mathbb{T}=(\mathbb{R}^{\infty}_{+},\min,+,\infty,0)$. The minimal cost to
obtain the query is $\min(1+5,1+8)=6$.

  * •

Assume that the facts are annotated with confidence scores $0.9$, $0.6$ and
$0.4$ respectively, from $\mathbb{V}=([0,1],\max,\times,0,1)$. The confidence
of the query answer is $\max(0.9\times 0.6,0.9\times 0.4)=0.54$.

  * •

Assume that the facts are annotated with truth values $0.9$, $0.8$, and $0.2$
respectively, from $\mathbb{F}=([0,1],\max,\min,0,1)$. The truth value of the
query is $\max(\min(0.9,0.8),\min(0.9,0.2))=0.8$.

  * •

Assume that the facts are annotated with truth degrees $0.9$, $0.8$, and $0.2$
respectively, from $\mathbb{L}=([0,1],\max,\star_{L},0,1)$. The truth value of
the query answer is $\max(\max(0,0.9+0.8-1),\max(0,0.9+0.2-1))=0.7$.

  * •

Assume that the facts are annotated with clearance levels $P$, $C$ and $S$
respectively, from $\mathbb{A}=(\\{P<C<S<T<0\\},\min,\max,0,P)$. The clearance
level required to derive the query is $\max(\min(P,C),\min(P,S))=C$. ∎

? (?) also define semiring provenance for Datalog queries, using derivation
trees. The approach associates to the query the sum over all its derivation
trees of the product of their leaf annotations. In this case, since there can
be infinitely many derivation trees, the semantics is well-defined only for a
restricted class of semirings, called _$\omega$ -continuous_ semirings. Given
a semiring $(K,\oplus,\otimes,\mathbb{0},\mathbb{1})$, let $\leq$ be the
binary relation over $K$ such that $a\leq b$ if and only if there exists $c\in
K$ with $a\oplus c=b$. A commutative semiring is _$\omega$ -continuous_ if
$\leq$ is a partial order, every (infinite) $\omega$-chain $a_{0}\leq
a_{1}\leq a_{2}\dots$ has a least upper bound
$\sup((a_{i})_{i\in\mathbb{N}})$, and for every $a\in K$,
$a\oplus\sup((a_{i})_{i\in\mathbb{N}})=\sup((a\oplus a_{i})_{i\in\mathbb{N}})$
and $a\otimes\sup((a_{i})_{i\in\mathbb{N}})=\sup((a\otimes
a_{i})_{i\in\mathbb{N}})$.

######  Example 2.5.

The counting semiring is the only semiring among those introduced in Example
2.3 that is not $\omega$-continuous. ∎

##### Provenance semirings

Provenance semirings were introduced to abstract from a specific semiring and
compute a representation of the provenance. Given a countably infinite set
${\sf X}$ of _variables_ that are used to annotate the database facts, a
_provenance semiring_ is a semiring over a space of _annotations_ , or
provenance expressions, with variables from ${\sf X}$.

A _semiring homomorphism_ from
$\mathbb{K}=(K,\oplus,\otimes,\mathbb{0},\mathbb{1})$ to
$\mathbb{K^{\prime}}=(K^{\prime},+,\cdot,0,1)$ is a mapping $h:K\rightarrow
K^{\prime}$ such that $h(\mathbb{0})=0$, $h(\mathbb{1})=1$, and for all
$a,b\in K$, $h(a\oplus b)=h(a)+h(b)$ and $h(a\otimes b)=h(a)\cdot h(b)$. A
semiring homomorphism between $\omega$-continuous semirings is _$\omega$
-continuous_ if it preserves least upper bounds:
$h(\sup((a_{i})_{i\in\mathbb{N}}))=\sup((h(a_{i}))_{i\in\mathbb{N}})$.

A provenance semiring $\mathit{Prov}({\sf X})$ _specializes_ correctly to a
semiring $\mathbb{K}$, if any valuation $\nu:{\sf X}\rightarrow K$ extends
uniquely to a ($\omega$-continuous if $\mathit{Prov}({\sf X})$ and
$\mathbb{K}$ are $\omega$-continuous) semiring homomorphism
$h:\mathit{Prov}({\sf X})\rightarrow K$, allowing the computations for
$\mathbb{K}$ to factor through the computations for $\mathit{Prov}({\sf X})$
(?, ?). A provenance semiring $\mathit{Prov}({\sf X})$ is _universal for a set
of semirings_ if it specializes correctly to each semiring of this set. ? (?)
showed that the so-called _provenance polynomials_ semiring $\mathbb{N}[{\sf
X}]=(\mathbb{N}[{\sf X}],+,\times,0,1)$ of polynomials with coefficients from
$\mathbb{N}$ and variables from ${\sf X}$, equipped with the usual operations,
is universal for commutative semirings.

$\mathbb{N}[{\sf X}]$$\mathbb{B}[{\sf X}]$$\sf{Sorp}[{\sf X}]$$\sf{Why}[{\sf
X}]$$\sf{PosBool}[{\sf X}]$$\sf{Lin}[{\sf X}]$$\sf{Trio}[{\sf
X}]$$\oplus$-idempotent$\otimes$-idempotentabsorptive$\otimes$-idempotent$\oplus$-idempotentabsorptive$\oplus\approx\otimes$$\otimes$-idempotent
Figure 1: A hierarchy of provenance semirings, see (?, Fig. 2).

Figure 1 shows the hierarchy of expressiveness for provenance annotations (?,
?, ?). The most expressive form of annotations for queries from the relational
algebra is provided by $\mathbb{N}[{\sf X}]$. Less general provenance
semirings are obtained by adding constraints such as idempotency of the
addition or multiplication, absorption, etc. Each of such provenance semiring
is universal for the class of semirings that respect the same constraints.

######  Example 2.6.

If we consider the semirings from Example 2.3 and the provenance semirings in
Figure 1, only $\mathbb{N}[{\sf X}]$ specializes correctly to the counting
semiring $(\mathbb{N},+,\times,0,1)$, while $\sf{Sorp}[{\sf X}]$ as well as
all provenance semirings above it specialize correctly to the tropical
semiring $(\mathbb{R}^{\infty}_{+},\min,+,\infty,0)$, the Viterbi semiring
$([0,1],\max,\times,0,1)$ and the Łukasiewicz semiring
$([0,1],\max,\star_{L},0,1)$, and $\sf{PosBool}[{\sf X}]$ as well as all
provenance semirings above it specialize correctly to the fuzzy semiring
$([0,1],\max,\min,0,1)$ and the access control semirings
$(\\{P<C<S<T<0\\},\min,\max,0,P)$ and $(L,\min,\max,\bot,\top)$. ∎

For Datalog queries, infinite provenance expressions may be needed. A formal
power series with variables from ${\sf X}$ and coefficients from $C$ is a
mapping that associates to each monomial over ${\sf X}$ a coefficient in $C$.
A formal power series $S$ can be written as a possibly infinite sum
$S=\Sigma_{m\in\mathsf{mon}({\sf X})}S(m)m$ where $\mathsf{mon}({\sf X})$ is
the set of all monomials over ${\sf X}$. $C\llbracket{\sf X}\rrbracket$
denotes the set of formal power series with variables from ${\sf X}$ and
coefficients from $C$. ? (?) define the _Datalog provenance semiring_ as
$\mathbb{N}^{\infty}\llbracket{\sf X}\rrbracket$, the commutative
$\omega$-continuous semiring of formal power series with coefficients from
$\mathbb{N}^{\infty}=\mathbb{N}\cup\\{\infty\\}$, and show that it is
universal for commutative $\omega$-continuous semirings. We can obtain a
hierarchy similar to that of Figure 1 where $\mathbb{N}[{\sf X}]$ is replaced
by $\mathbb{N}^{\infty}\llbracket{\sf X}\rrbracket$, $\mathbb{B}[{\sf X}]$ is
replaced by the semiring of formal power series with Boolean coefficient
$\mathbb{B}\llbracket{\sf X}\rrbracket$ etc.

In this work, we will mostly focus on the provenance semirings $\sf{Why}[{\sf
X}]$, $\sf{PosBool}[{\sf X}]$ and $\sf{Lin}[{\sf X}]$—which all require both
operations to be idempotent—and discuss the difficulties that arise for more
expressive provenance semirings. These provenance semirings correspond to
notions of query explanation that have long been considered in the context of
databases: $\sf{Why}[{\sf X}]$ corresponds to the _why-provenance_ , or
_witness basis_ , $\sf{PosBool}[{\sf X}]$ corresponds to the _minimal witness
basis_ , and $\sf{Lin}[{\sf X}]$ corresponds to _lineage_ (?, ?).

##  3 Semiring Provenance for Description Logics

In this section, we define a provenance semantics for ${\cal E\\!LHI}_{\bot}$
ontologies and discuss its properties. In particular, we investigate whether
it captures some well-known semantics for ontologies annotated with specific
kinds of information and whether it extends the notions of provenance defined
for relational and Datalog queries in the database setting, among other
desirable properties. We also discuss the restrictions of our setting.

###  3.1 Provenance Semantics for Annotated Ontologies

Let $\mathbb{K}=(K,\oplus,\otimes,\mathbb{0},\mathbb{1})$ be a commutative
$\omega$-continuous semiring and $\mathcal{L}$ be a DL language encompassed by
${\cal E\\!LHI}_{\bot}$. A _( $\mathbb{K}$-)annotated $\mathcal{L}$ ontology_
$\mathcal{O}^{\mathbb{K}}$ is a pair $\langle\mathcal{O},\lambda\rangle$ where
$\mathcal{O}$ is an $\mathcal{L}$ ontology and $\lambda$ is an annotation
function $\lambda:\mathcal{O}\mapsto K\setminus\\{\mathbb{0}\\}$. We often
treat $\mathcal{O}^{\mathbb{K}}$ as the set of pairs
$\\{(\alpha,\lambda(\alpha))\mid\alpha\in\mathcal{O}\\}$ and call such pairs
$(\alpha,\lambda(\alpha))$ _annotated axioms_.

The semantics of annotated ontologies extends the classical notion of
interpretations with annotations. A _( $\mathbb{K}$-)annotated interpretation_
is a triple $\mathcal{I}=(\Delta^{\mathcal{I}},K,\cdot^{\mathcal{I}})$ where
$\Delta^{\mathcal{I}}$ is a non-empty set (the _domain_ of $\mathcal{I}$), and
$\cdot^{\mathcal{I}}$ maps

  * •

every $a\in{\sf N_{I}}$ to $a^{\mathcal{I}}\in\Delta^{\mathcal{I}}$;

  * •

every $A\in{\sf N_{C}}$ to a countable
$A^{\mathcal{I}}\subseteq\Delta^{\mathcal{I}}\times K$;

  * •

every $R\in{\sf N_{R}}$ to a countable
$R^{\mathcal{I}}\subseteq\Delta^{\mathcal{I}}\times\Delta^{\mathcal{I}}\times
K$.

We extend $\cdot^{\mathcal{I}}$ to complex expressions as follows:

$\displaystyle(\top)^{\mathcal{I}}={}$
$\displaystyle\Delta^{\mathcal{I}}\times\\{\mathbb{1}\\};$
$\displaystyle(\bot)^{\mathcal{I}}={}$ $\displaystyle\emptyset;$
$\displaystyle(R^{-})^{\mathcal{I}}={}$
$\displaystyle\\{(e,d,\kappa)\mid(d,e,\kappa)\in R^{\mathcal{I}}\\};$
$\displaystyle(\exists P.C)^{\mathcal{I}}={}$
$\displaystyle\\{(d,\kappa\otimes\kappa^{\prime})\mid\exists
e\in\Delta^{\mathcal{I}}\text{ s.t. }(d,e,\kappa)\in
R^{\mathcal{I}},(e,\kappa^{\prime})\in C^{\mathcal{I}}\\};$
$\displaystyle(C\sqcap D)^{\mathcal{I}}={}$
$\displaystyle\\{(d,\kappa\otimes\kappa^{\prime})\mid(d,\kappa)\in
C^{\mathcal{I}},(d,\kappa^{\prime})\in D^{\mathcal{I}}\\}.$

The annotated interpretation $\mathcal{I}$ _satisfies_ :

$\displaystyle({C\sqsubseteq D},{\kappa}),$ $\displaystyle\text{if
}(d,\kappa^{\prime})\in C^{\mathcal{I}}\text{ implies
}(d,\kappa\otimes\kappa^{\prime})\in D^{\mathcal{I}}\\!;$
$\displaystyle({P\sqsubseteq Q},{\kappa}),$ $\displaystyle\text{if
}(d,e,\kappa^{\prime})\in P^{\mathcal{I}}\text{ implies
}(d,e,\kappa\otimes\kappa^{\prime})\in Q^{\mathcal{I}}\\!;$
$\displaystyle({P\sqcap Q\sqsubseteq\bot},{\kappa}),$ $\displaystyle\text{if
}P^{\mathcal{I}}\cap Q^{\mathcal{I}}=\emptyset;$
$\displaystyle({A(a)},{\kappa}),$ $\displaystyle\text{if
}(a^{\mathcal{I}},\kappa)\in A^{\mathcal{I}}\\!;\quad\text{ and }$
$\displaystyle({R(a,b)},{\kappa}),$ $\displaystyle\text{if
}(a^{\mathcal{I}},b^{\mathcal{I}},\kappa)\in R^{\mathcal{I}}\\!.$

Remark that since $\bot^{\mathcal{I}}=\emptyset$, the satisfaction of a GCI of
the form $(C\sqsubseteq\bot,\kappa)$ (i.e. $(d,\kappa^{\prime})\in
C^{\mathcal{I}}$ implies
$(d,\kappa\otimes\kappa^{\prime})\in\bot^{\mathcal{I}}$) is equivalent to
$C^{\mathcal{I}}=\emptyset$, which is similar to the satisfaction of negative
role inclusion $(P\sqcap Q\sqsubseteq\bot,\kappa)$.

The interpretation of a concept (resp. role) name may contain several pairs
$(d,\kappa)$ (resp. triples $(d,e,\kappa)$) with the same domain element
$d\in\Delta^{\mathcal{I}}$ (resp. elements $d,e\in\Delta^{\mathcal{I}}$),
allowing for several provenance annotations to be dealt with simultaneously.

$\mathcal{I}$ is a model of the annotated ontology $\mathcal{O}^{\mathbb{K}}$,
denoted $\mathcal{I}\models\mathcal{O}^{\mathbb{K}}$, if it satisfies all
annotated axioms in $\mathcal{O}^{\mathbb{K}}$. $\mathcal{O}^{\mathbb{K}}$
_entails_ $(\alpha,\kappa)$, denoted
$\mathcal{O}^{\mathbb{K}}\models(\alpha,\kappa)$, if
$\mathcal{I}\models(\alpha,\kappa)$ for every model $\mathcal{I}$ of
$\mathcal{O}^{\mathbb{K}}$. The _provenance annotations_ of $\alpha$ in
$\mathcal{I}$ is the set ${\sf
prov}_{\mathcal{I}}({\alpha})=\\{\kappa\mid\mathcal{I}\models(\alpha,\kappa)\\}$.
In the following we sometimes write $\bigoplus_{S}$ to denote the semiring
addition over the elements of $S$. We define the _provenance_ of $\alpha$
w.r.t. a satisfiable $\mathcal{O}^{\mathbb{K}}$ as

$\displaystyle\mathcal{P}(\alpha,\mathcal{O}^{\mathbb{K}}):=\bigoplus_{\kappa\in\bigcap_{\mathcal{I}\models\mathcal{O}^{\mathbb{K}}}{\sf
prov}_{\mathcal{I}}({\alpha})}\kappa=\bigoplus_{\mathcal{O}^{\mathbb{K}}\models(\alpha,\kappa)}\kappa.$
(1)

For unsatisfiable $\mathcal{O}^{\mathbb{K}}$ we define
$\mathcal{P}(\alpha,\mathcal{O}^{\mathbb{K}}):=\bigoplus_{\kappa\in K}\kappa$,
as $\mathcal{O}^{\mathbb{K}}\models(\alpha,\kappa)$ for every $\kappa\in K$.

######  Remark 3.1.

If the sum in Equation (1) is empty (i.e. no $\kappa\in K$ is such that
$\mathcal{O}^{\mathbb{K}}\models(\alpha,\kappa)$) then
$\mathcal{P}(\alpha,\mathcal{O}^{\mathbb{K}}):=\mathbb{0}$. In the other
extreme, if it is infinite, which can happen when semiring operations are not
idempotent, the sum is well-defined due to the $\omega$-continuity of
$\mathbb{K}$.

######  Remark 3.2 (Unsatisfiable concept/role).

If an ${\cal E\\!LHI}_{\bot}$ concept $C$ is unsatisfiable w.r.t.
$\mathcal{O}$, i.e. such that for every model $\mathcal{I}$ of $\mathcal{O}$,
$C^{\mathcal{I}}=\emptyset$, then for every $\omega$-continuous semiring
$(K,\oplus,\otimes,\mathbb{0},\mathbb{1})$, annotated version
$\mathcal{O}^{\mathbb{K}}=\langle\mathcal{O},\lambda\rangle$, ${\cal
E\\!LHI}_{\bot}$ concept $D$ and $\kappa\in K$, it holds that
$\mathcal{O}^{\mathbb{K}}\models(C\sqsubseteq D,\kappa)$, so that
$\mathcal{P}(C\sqsubseteq D,\mathcal{O}^{\mathbb{K}})=\bigoplus_{\kappa\in
K}\kappa$. The same hold for unsatisfiable roles. This is not a problem since
GCI or RI with an unsatisfiable concept or role in the left-hand side
trivially holds so we are not interested in computing their provenance.

######  Remark 3.3.

We could have defined annotated interpretations without requiring the
interpretations of concept and role names to be countable (allowing for
example an $\mathbb{F}$-annotated interpretation where
$A^{\mathcal{I}}=\\{(a,n)\mid 0\leq n<0.5\\}$) without any impact on the
provenance definition. Indeed, every annotated ontology has some annotated
models that interpret concept and role names by countable sets (in particular,
its canonical model introduced in Section 3.4), so the set of semiring
elements over which the sum is made in Equation (1) would be countable anyway.
We choose to consider only countable annotations for simplicity, since
uncountable ones do not bring anything regarding provenance.

######  Example 3.4.

Consider the following ontology:

$\displaystyle\mathcal{O}=\\{$
$\displaystyle\mathsf{Deity}(\mathsf{Dionysus}),\mathsf{mother}(\mathsf{Dionysus},\mathsf{Semele}),\mathsf{mother}(\mathsf{Dionysus},\mathsf{Demeter}),$
$\displaystyle\mathsf{Deity}(\mathsf{Demeter}),\mathsf{father}(\mathsf{Dionysus},\mathsf{Zeus}),\mathsf{Deity}(\mathsf{Zeus}),$
$\displaystyle\exists\mathsf{parent}.\mathsf{Deity}\sqsubseteq\mathsf{Deity},\mathsf{mother}\sqsubseteq\mathsf{parent},\mathsf{father}\sqsubseteq\mathsf{parent}\\}.$

We define the annotated ontologies $\mathcal{O}^{\sf{Why}[{\sf
X}]}=\langle\mathcal{O},\lambda_{\sf X}\rangle$,
$\mathcal{O}^{\mathbb{T}}=\langle\mathcal{O},\lambda_{\mathbb{T}}\rangle$, and
$\mathcal{O}^{\mathbb{F}}=\langle\mathcal{O},\lambda_{\mathbb{F}}\rangle$,
annotated with variables, costs and truth degrees respectively, as follows.

| $\lambda_{\sf X}$ | $\lambda_{\mathbb{T}}$ | $\lambda_{\mathbb{F}}$
---|---|---|---
$\mathsf{Deity}$($\mathsf{Dionysus}$) | $x_{1}$ | 1 | 0.9
$\mathsf{mother}$($\mathsf{Dionysus}$,$\mathsf{Semele}$) | $x_{2}$ | 5 | 0.8
$\mathsf{mother}$($\mathsf{Dionysus}$,$\mathsf{Demeter}$) | $x_{3}$ | 8 | 0.2
$\mathsf{Deity}$($\mathsf{Demeter}$) | $x_{4}$ | 1 | 0.9
$\mathsf{father}$($\mathsf{Dionysus}$,$\mathsf{Zeus}$) | $x_{5}$ | 2 | 0.9
$\mathsf{Deity}$($\mathsf{Zeus}$) | $x_{6}$ | 1 | 1
$\exists\mathsf{parent}.\mathsf{Deity}\sqsubseteq\mathsf{Deity}$ | $y_{1}$ | 2 | 0.5
$\mathsf{mother}\sqsubseteq\mathsf{parent}$ | $y_{2}$ | 1 | 1
$\mathsf{father}\sqsubseteq\mathsf{parent}$ | $y_{3}$ | 1 | 1

Let $\mathcal{I}^{\sf X}$ be a ${\sf{Why}[{\sf X}]}$-annotated interpretation
such that $\mathcal{I}^{\sf X}\models\mathcal{O}^{\sf{Why}[{\sf X}]}$.

  * •

Since $\mathcal{I}^{\sf X}\models(\mathsf{Deity}(\mathsf{Dionysus}),x_{1})$,
then $(\mathsf{Dionysus}^{\mathcal{I}^{\sf
X}},x_{1})\in\mathsf{Deity}^{\mathcal{I}^{\sf X}}$.

  * •

Since $\mathcal{I}^{\sf
X}\models(\mathsf{mother}(\mathsf{Dionysus},\mathsf{Demeter}),x_{3})$,
$(\mathsf{Dionysus}^{\mathcal{I}^{\sf X}},\mathsf{Demeter}^{\mathcal{I}^{\sf
X}},x_{3})\in\mathsf{mother}^{\mathcal{I}^{\sf X}}$. So $\mathcal{I}^{\sf
X}\models(\mathsf{mother}\sqsubseteq\mathsf{parent},y_{2})$ yields
$(\mathsf{Dionysus}^{\mathcal{I}^{\sf X}},\mathsf{Demeter}^{\mathcal{I}^{\sf
X}},x_{3}y_{2})\in\mathsf{parent}^{\mathcal{I}^{\sf X}}$. Moreover,
$\mathcal{I}^{\sf X}\models(\mathsf{Deity}(\mathsf{Demeter}),x_{4})$ implies
$(\mathsf{Demeter}^{\mathcal{I}^{\sf
X}},x_{4})\in\mathsf{Deity}^{\mathcal{I}^{\sf X}}$. Hence from
$\mathcal{I}^{\sf
X}\models(\exists\mathsf{parent}.\mathsf{Deity}\sqsubseteq\mathsf{Deity},y_{1})$
one obtains $(\mathsf{Dionysus}^{\mathcal{I}^{\sf
X}},x_{3}x_{4}y_{1}y_{2})\in\mathsf{Deity}^{\mathcal{I}^{\sf X}}$.

  * •

Similarly, since we have $\mathcal{I}^{\sf
X}\models(\mathsf{father}(\mathsf{Dionysus},\mathsf{Zeus}),x_{5})$,
$\mathcal{I}^{\sf X}\models(\mathsf{Deity}(\mathsf{Zeus}),x_{6})$, and
$\mathcal{I}^{\sf X}\models(\mathsf{father}\sqsubseteq\mathsf{parent},y_{3})$
it holds that $(\mathsf{Dionysus}^{\mathcal{I}^{\sf
X}},x_{5}x_{6}y_{1}y_{3})\in\mathsf{Deity}^{\mathcal{I}^{\sf X}}$.

Hence, it holds that $\mathcal{O}^{\sf{Why}[{\sf
X}]}\models(\mathsf{Deity}(\mathsf{Dionysus}),x_{1})$,
$\mathcal{O}^{\sf{Why}[{\sf
X}]}\models(\mathsf{Deity}(\mathsf{Dionysus}),x_{3}x_{4}y_{1}y_{2})$,
$\mathcal{O}^{\sf{Why}[{\sf
X}]}\models(\mathsf{Deity}(\mathsf{Dionysus}),x_{5}x_{6}y_{1}y_{3})$, and the
provenance of $\mathsf{Deity}(\mathsf{Dionysus})$ w.r.t.
$\mathcal{O}^{\sf{Why}[{\sf X}]}$ is
$\mathcal{P}(\mathsf{Deity}(\mathsf{Dionysus}),\mathcal{O}^{\sf{Why}[{\sf
X}]})=x_{1}+x_{3}x_{4}y_{1}y_{2}+x_{5}x_{6}y_{1}y_{3}$.

We obtain the following results similarly, by considering
$\mathbb{T}$-annotated and $\mathbb{F}$-annotated interpretations that are
models of $\mathcal{O}^{\mathbb{T}}$ and $\mathcal{O}^{\mathbb{F}}$
respectively. Recall that the multiplication of the tropical semiring
$\mathbb{T}$ is the usual addition and its addition is $\min$, while the
multiplication of the fuzzy semiring $\mathbb{F}$ is $\min$ and its addition
is $\max$.

  * •

$\mathcal{O}^{\mathbb{T}}\models(\mathsf{Deity}(\mathsf{Dionysus}),1)$,
$\mathcal{O}^{\mathbb{T}}\models(\mathsf{Deity}(\mathsf{Dionysus}),12)$,
$\mathcal{O}^{\mathbb{T}}\models(\mathsf{Deity}(\mathsf{Dionysus}),6)$, and
$\mathcal{P}(\mathsf{Deity}(\mathsf{Dionysus}),\mathcal{O}^{\mathbb{T}})=1$;

  * •

$\mathcal{O}^{\mathbb{F}}\models(\mathsf{Deity}(\mathsf{Dionysus}),0.9)$,
$\mathcal{O}^{\mathbb{F}}\models(\mathsf{Deity}(\mathsf{Dionysus}),0.2)$,
$\mathcal{O}^{\mathbb{F}}\models(\mathsf{Deity}(\mathsf{Dionysus}),0.5)$, and
$\mathcal{P}(\mathsf{Deity}(\mathsf{Dionysus}),\mathcal{O}^{\mathbb{F}})=0.9$.
∎

######  Definition 3.5.

A (classical) interpretation
$\mathcal{I}=(\Delta^{\mathcal{I}},\cdot^{\mathcal{I}})$ and a
$\mathbb{K}$-annotated interpretation
$\mathcal{I}^{\mathbb{K}}=(\Delta^{\mathcal{I}^{\mathbb{K}}},K,\cdot^{\mathcal{I}^{\mathbb{K}}})$
_coincide on their non-annotated part_ iff (i)
$\Delta^{\mathcal{I}}=\Delta^{\mathcal{I}^{\mathbb{K}}}$; (ii) for all
$a\in{\sf N_{I}}$, $a^{\mathcal{I}}=a^{\mathcal{I}^{\mathbb{K}}}$; (iii) for
all $A\in{\sf N_{C}}$ and $d\in\Delta^{\mathcal{I}}$, it holds that $d\in
A^{\mathcal{I}}$ iff there exists $\kappa\in K$ such that $(d,\kappa)\in
A^{\mathcal{I}^{\mathbb{K}}}$; and (iv) for all $R\in{\sf N_{R}}$ and
$d,e\in\Delta^{\mathcal{I}}$, it holds that $(d,e)\in R^{\mathcal{I}}$ iff
there exists $\kappa\in K$ such that $(d,e,\kappa)\in
R^{\mathcal{I}^{\mathbb{K}}}$.

The next lemma shows how annotated and non-annotated models are related, and
that satisfiability does not depend on the annotations.

######  Lemma 3.6.

Let $\mathcal{O}^{\mathbb{K}}=\langle\mathcal{O},\lambda\rangle$ be a
$\mathbb{K}$-annotated ontology. The following claims hold.

  1. (i)

For every model $\mathcal{I}$ of $\mathcal{O}$, there exists a model
$\mathcal{I}^{\mathbb{K}}$ of $\mathcal{O}^{\mathbb{K}}$ such that
$\mathcal{I}$ and $\mathcal{I}^{\mathbb{K}}$ coincide on their non-annotated
part.

  2. (ii)

For every model $\mathcal{I}^{\mathbb{K}}$ of $\mathcal{O}^{\mathbb{K}}$ there
exists a model $\mathcal{I}$ of $\mathcal{O}$ such that $\mathcal{I}$ and
$\mathcal{I}^{\mathbb{K}}$ coincide on their non-annotated part.

###  3.2 Querying Annotated Ontologies

To define the provenance of (Boolean) CQs, we consider _extended CQs_ , which
replace concept and role predicates with binary and ternary predicates
respectively, where the last term of the tuple is used for expressing
provenance information. Given a CQ
$q(\vec{x})=\exists\vec{y}\,\phi(\vec{x},\vec{y})$, its _extended version_ is
$\boldsymbol{q}(\vec{x})=\exists\vec{y}\exists\vec{t}\,\phi^{\prime}(\vec{x},\vec{y},\vec{t})$
where $\vec{t}$ is a tuple of variables disjoint from $\vec{x}\cup\vec{y}$ and
$\phi^{\prime}(\vec{x},\vec{y},\vec{t})$ is obtained from
$\phi(\vec{x},\vec{y})$ by replacing each $A(x)$ by $A(x,t)$ and each
$R(x_{1},x_{2})$ by $R(x_{1},x_{2},t)$ with $t\in\vec{t}$ such that $t$ does
not occur anywhere else in $\phi^{\prime}(\vec{x},\vec{y},\vec{t})$ (we assume
a scheme for assigning variables that ensures “the extended version” is well
defined). We use $P(\vec{x},t)$ to refer to an atom which is either
$A(x_{1},t)$ or $R(x_{1},x_{2},t)$, and $P(\vec{x},t)\in\boldsymbol{q}$ if
$P(\vec{x},t)$ occurs in $\boldsymbol{q}$. A $\mathbb{K}$-annotated
interpretation $\mathcal{I}$ satisfies an extended BCQ
$\boldsymbol{q}:=\exists\vec{y}\,\phi(\vec{y})$, written
$\mathcal{I}\models\boldsymbol{q}$, iff there is a _match for $\boldsymbol{q}$
in $\mathcal{I}$_, where a match for $\boldsymbol{q}$ in $\mathcal{I}$ is a
function
$\pi:\mathsf{terms}(\boldsymbol{q})\rightarrow\Delta^{\mathcal{I}}\cup K$ such
that $\pi(t)=t^{\mathcal{I}}$ for every $t\in{\sf N_{I}}$, and
$\pi(\vec{t},t)\in P^{\mathcal{I}}$ for every
$P(\vec{t},t)\in\mathsf{atoms}(\boldsymbol{q})$, where $\pi(\vec{t},t)$ is a
shorthand for $(\pi(t_{1}),\pi(t))$ or $(\pi(t_{1}),\pi(t_{2}),\pi(t))$
depending on the arity of $P$. An extended BCQ $\boldsymbol{q}$ is _entailed_
by an annotated ontology $\mathcal{O}^{\mathbb{K}}$, written
$\mathcal{O}^{\mathbb{K}}\models\boldsymbol{q}$, if and only if
$\mathcal{I}\models\boldsymbol{q}$ for every model $\mathcal{I}$ of
$\mathcal{O}^{\mathbb{K}}$. The following proposition is a direct consequence
of the definition of (extended) BCQ entailment and Lemma 3.6.

######  Proposition 3.7.

For every annotated ontology $\mathcal{O}^{\mathbb{K}}$ and BCQ $q$,
$\mathcal{O}\models q$ iff $\mathcal{O}^{\mathbb{K}}\models\boldsymbol{q}$
where $\boldsymbol{q}$ is the extended version of $q$.

Given an extended BCQ $\boldsymbol{q}$ and a $\mathbb{K}$-annotated
interpretation $\mathcal{I}$, let $\nu_{\mathcal{I}}(\boldsymbol{q})$ denote
the set of all matches of $\boldsymbol{q}$ in $\mathcal{I}$. The _provenance
annotations_ of $\boldsymbol{q}$ on $\mathcal{I}$ is defined as the set ${\sf
prov}_{\mathcal{I}}({\boldsymbol{q}})=\left\\{\bigotimes_{P(\vec{t},t)\in\boldsymbol{q}}\pi(t)\mid\pi\in\nu_{\mathcal{I}}(\boldsymbol{q})\right\\}$
of elements of $\mathbb{K}$, where $\pi(t)$ is the last element of the tuple
$\pi(\vec{t},t)\in P^{\mathcal{I}}$. We define the _provenance_ of
$\boldsymbol{q}$ w.r.t. $\mathcal{O}^{\mathbb{K}}$ as

$\displaystyle\mathcal{P}(\boldsymbol{q},\mathcal{O}^{\mathbb{K}}):=\bigoplus_{\kappa\in\bigcap_{\mathcal{I}\models\mathcal{O}^{\mathbb{K}}}{\sf
prov}_{\mathcal{I}}({\boldsymbol{q}})}\kappa.$

The provenance of a BCQ $q$ w.r.t. $\mathcal{O}^{\mathbb{K}}$ is defined as
$\mathcal{P}(q,\mathcal{O}^{\mathbb{K}}):=\mathcal{P}(\boldsymbol{q},\mathcal{O}^{\mathbb{K}})$
where $\boldsymbol{q}$ is the extended version of $q$. We write $(q,\kappa)$
to denote an _annotated BCQ_. The semantics of annotated BCQs is as expected:
$\mathcal{I}\models(q,\kappa)$ if $\kappa\in{\sf
prov}_{\mathcal{I}}({\boldsymbol{q}})=\left\\{\bigotimes_{P(\vec{t},t)\in\boldsymbol{q}}\pi(t)\mid\pi\in\nu_{\mathcal{I}}(\boldsymbol{q})\right\\}$,
and $\mathcal{O}^{\mathbb{K}}\models(q,\kappa)$ if
$\mathcal{I}\models\mathcal{O}^{\mathbb{K}}$ implies
$\mathcal{I}\models(q,\kappa)$, for all $\mathbb{K}$-annotated interpretations
$\mathcal{I}$. Hence

$\displaystyle\mathcal{P}(q,\mathcal{O}^{\mathbb{K}})=\mathcal{P}(\boldsymbol{q},\mathcal{O}^{\mathbb{K}})=\bigoplus_{\kappa\in\bigcap_{\mathcal{I}\models\mathcal{O}^{\mathbb{K}}}{\sf
prov}_{\mathcal{I}}({\boldsymbol{q}})}\kappa=\bigoplus_{\mathcal{O}^{\mathbb{K}}\models(q,\kappa)}\kappa.$

Recall that interpretations always map semiring values to themselves; hence
the use of the third value in the tuples of the query or of the interpretation
is formally correct. This should become more clear with the following example.

######  Example 3.8 (Example 3.4 continued).

Consider the extended version of the query that asks for the deities having
some parent, $\boldsymbol{q}(x)=\exists
yt_{1}t_{2}\,\mathsf{Deity}(x,t_{1})\wedge\mathsf{parent}(x,y,t_{2})$.

We saw in Example 3.4 that all models $\mathcal{I}^{\sf X}$ of
$\mathcal{O}^{\sf{Why}[{\sf X}]}$ satisfy
$(\mathsf{Dionysus}^{\mathcal{I}^{\sf
X}},x_{1})\in\mathsf{Deity}^{\mathcal{I}^{\sf X}}$,
$(\mathsf{Dionysus}^{\mathcal{I}^{\sf
X}},x_{3}x_{4}y_{1}y_{2})\in\mathsf{Deity}^{\mathcal{I}^{\sf X}}$, and
$(\mathsf{Dionysus}^{\mathcal{I}^{\sf
X}},x_{5}x_{6}y_{1}y_{3})\in\mathsf{Deity}^{\mathcal{I}^{\sf X}}$. In
addition, it holds that $(\mathsf{Dionysus}^{\mathcal{I}^{\sf
X}},\mathsf{Demeter}^{\mathcal{I}^{\sf
X}},x_{3}y_{2})\in\mathsf{parent}^{\mathcal{I}^{\sf X}}$ and
$(\mathsf{Dionysus}^{\mathcal{I}^{\sf X}},\mathsf{Zeus}^{\mathcal{I}^{\sf
X}},x_{5}y_{3})\in\mathsf{parent}^{\mathcal{I}^{\sf X}}$. It also holds that
$(\mathsf{Dionysus}^{\mathcal{I}^{\sf X}},\mathsf{Semele}^{\mathcal{I}^{\sf
X}},x_{2}y_{2})\in\mathsf{parent}^{\mathcal{I}^{\sf X}}$. Hence, for every
model $\mathcal{I}^{\sf X}$ of $\mathcal{O}^{\sf{Why}[{\sf X}]}$, there are
the following matches for $\boldsymbol{q}(\mathsf{Dionysus})$ in
$\mathcal{I}^{\sf X}$:

  * •

$\pi_{1}(\mathsf{Dionysus})=\mathsf{Dionysus}^{\mathcal{I}^{\sf X}}$,
$\pi_{1}(y)=\mathsf{Semele}^{\mathcal{I}^{\sf X}}$, $\pi_{1}(t_{1})=x_{1}$,
$\pi_{1}(t_{2})=x_{2}y_{2}$;

  * •

$\pi_{2}(\mathsf{Dionysus})=\mathsf{Dionysus}^{\mathcal{I}^{\sf X}}$,
$\pi_{2}(y)=\mathsf{Demeter}^{\mathcal{I}^{\sf X}}$, $\pi_{2}(t_{1})=x_{1}$,
$\pi_{2}(t_{2})=x_{3}y_{2}$;

  * •

$\pi_{3}(\mathsf{Dionysus})=\mathsf{Dionysus}^{\mathcal{I}^{\sf X}}$,
$\pi_{3}(y)=\mathsf{Zeus}^{\mathcal{I}^{\sf X}}$, $\pi_{3}(t_{1})=x_{1}$,
$\pi_{3}(t_{2})=x_{5}y_{3}$;

  * •

$\pi_{4}(\mathsf{Dionysus})=\mathsf{Dionysus}^{\mathcal{I}^{\sf X}}$,
$\pi_{4}(y)=\mathsf{Semele}^{\mathcal{I}^{\sf X}}$,
$\pi_{4}(t_{1})=x_{3}x_{4}y_{1}y_{2}$, $\pi_{4}(t_{2})=x_{2}y_{2}$;

  * •

$\pi_{5}(\mathsf{Dionysus})=\mathsf{Dionysus}^{\mathcal{I}^{\sf X}}$,
$\pi_{5}(y)=\mathsf{Demeter}^{\mathcal{I}^{\sf X}}$,
$\pi_{5}(t_{1})=x_{3}x_{4}y_{1}y_{2}$, $\pi_{5}(t_{2})=x_{3}y_{2}$;

  * •

$\pi_{6}(\mathsf{Dionysus})=\mathsf{Dionysus}^{\mathcal{I}^{\sf X}}$,
$\pi_{6}(y)=\mathsf{Zeus}^{\mathcal{I}^{\sf X}}$,
$\pi_{6}(t_{1})=x_{3}x_{4}y_{1}y_{2}$, $\pi_{6}(t_{2})=x_{5}y_{3}$;

  * •

$\pi_{7}(\mathsf{Dionysus})=\mathsf{Dionysus}^{\mathcal{I}^{\sf X}}$,
$\pi_{7}(y)=\mathsf{Semele}^{\mathcal{I}^{\sf X}}$,
$\pi_{7}(t_{1})=x_{5}x_{6}y_{1}y_{3}$, $\pi_{7}(t_{2})=x_{2}y_{2}$;

  * •

$\pi_{8}(\mathsf{Dionysus})=\mathsf{Dionysus}^{\mathcal{I}^{\sf X}}$,
$\pi_{8}(y)=\mathsf{Demeter}^{\mathcal{I}^{\sf X}}$,
$\pi_{8}(t_{1})=x_{5}x_{6}y_{1}y_{3}$, $\pi_{8}(t_{2})=x_{3}y_{2}$;

  * •

$\pi_{9}(\mathsf{Dionysus})=\mathsf{Dionysus}^{\mathcal{I}^{\sf X}}$,
$\pi_{9}(y)=\mathsf{Zeus}^{\mathcal{I}^{\sf X}}$,
$\pi_{9}(t_{1})=x_{5}x_{6}y_{1}y_{3}$, $\pi_{9}(t_{2})=x_{5}y_{3}$.

It follows that
$\mathcal{P}(\boldsymbol{q}(\mathsf{Dionysus}),\mathcal{O}^{\sf{Why}[{\sf
X}]})=x_{1}x_{2}y_{2}+x_{1}x_{3}y_{2}+x_{1}x_{5}y_{3}+x_{3}x_{4}y_{1}y_{2}x_{2}+x_{3}x_{4}y_{1}y_{2}+x_{3}x_{4}y_{1}y_{2}x_{5}y_{3}+x_{5}x_{6}y_{1}y_{3}x_{2}y_{2}+x_{5}x_{6}y_{1}y_{3}x_{3}y_{2}+x_{5}x_{6}y_{1}y_{3}$.

We obtain the following results similarly, by considering the matches for
$\boldsymbol{q}(\mathsf{Dionysus})$ in the $\mathbb{T}$-annotated and
$\mathbb{F}$-annotated interpretations that are models of
$\mathcal{O}^{\mathbb{T}}$ and $\mathcal{O}^{\mathbb{F}}$ respectively.

  * •

$\mathcal{P}(\boldsymbol{q}(\mathsf{Dionysus}),\mathcal{O}^{\mathbb{T}})=4$;

  * •

$\mathcal{P}(\boldsymbol{q}(\mathsf{Dionysus}),\mathcal{O}^{\mathbb{F}})=0.9$.
∎

It is well-known that there is a one-to-one correspondance between ${\cal
E\\!LHI}_{\bot}$ concepts and rooted tree-shaped queries: given an ${\cal
E\\!LHI}_{\bot}$ concept $C$, there is a rooted tree-shaped query $q_{C}(x)$
that retrieves all instances of $C$ and can be build by structural induction
on $C$; and given a rooted tree-shaped query $q(x)$, there is an ${\cal
E\\!LHI}_{\bot}$ concept $C_{q}$ such that $q(x)$ retrieves all instances of
$C_{q}$ and $C_{q}$ can be build by structural induction on the tree-structure
of $q(x)$. The following lemma establishes the relationship between the
answers of $\boldsymbol{q_{C}}(x)$ and their provenance annotations in an
interpretation and the interpretation of $C$.

######  Lemma 3.9.

For every ${\cal E\\!LHI}_{\bot}$ concept $C$, if $\boldsymbol{q_{C}}(x)$ is
the extended version of the rooted tree-shaped query ${q_{C}}(x)$, then for
every annotated interpretation $\mathcal{I}$ and for every
$d\in\Delta^{\mathcal{I}}$, we have that
$\\{\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\\}=\\{\kappa\mid(d,\kappa)\in
C^{\mathcal{I}}\\}$.

Theorem 3.10 establishes that computing the provenance of query answers for
CQs that are tree-shaped and rooted can be reduced to computing the provenance
of assertions in polynomial time. This allows us to extend all results given
for assertion entailment in this paper to such CQs.

######  Theorem 3.10.

For every annotated ${\cal E\\!LHI}_{\bot}$ ontology
$\mathcal{O}^{\mathbb{K}}$, ${\cal E\\!LHI}_{\bot}$ concept $C$ and $a\in{\sf
N_{I}}$, we have
$\mathcal{P}(q_{C}(a),\mathcal{O}^{\mathbb{K}})=\mathcal{P}(A_{C}(a),\mathcal{O}^{\mathbb{K}}\cup\\{(C\sqsubseteq
A_{C},\mathbb{1})\\})$, where $A_{C}$ is a fresh concept name.

###  3.3 Relationship with Semantics for Specific Annotations

We now discuss some weighted reasoning tasks which have been studied in the
literature, and show how some of them fall into our general approach.
Regarding the use of provenance as explanation, we will discuss in details in
Section 5.1 the relationship between our provenance semantics and one of the
most studied related problems in the DL community, axiom pinpointing (?).

##### Fuzzy DL

The original work on fuzzy DLs introduced by ? (?) considers fuzzy assertions
of the form $(\alpha,n)$ where $n\in[0,1]$ represents the membership degree
for the assertion $\alpha$, and the terminological axioms are all considered
to be classical; that is, they are precise. Fuzzy interpretations generalise
classical interpretations by considering concepts and roles as _fuzzy_ unary
and binary predicates, respectively. More precisely, every concept name
$A\in{\sf N_{C}}$ is interpreted as a function
$A^{\mathcal{I}}:\Delta^{\mathcal{I}}\to[0,1]$ and likewise role names
$R\in{\sf N_{R}}$ are interpreted as (binary) functions
$R^{\mathcal{I}}:\Delta^{\mathcal{I}}\times\Delta^{\mathcal{I}}\to[0,1]$.
Following the then-popular Zadeh semantics (?), which for the scope of ${\cal
E\\!LHI}_{\bot}$ in the setting of ? coincides with the standard Gödel
semantics of mathematical fuzzy logic (?), conjunctions are interpreted
through the minimum ($\min$) operator over the interval $[0,1]$, while
disjunctions and existential restrictions are based on the maximum ($\max$). A
GCI $C\sqsubseteq D$ is satisfied by a fuzzy interpretation $\mathcal{I}$ iff
the membership degree for $C$ is less than or equal to the degree for $D$ at
every domain element; i.e., if for every $d\in\Delta^{\mathcal{I}}$ it holds
that $C^{\mathcal{I}}(d)\leq D^{\mathcal{I}}(d)$. The entailment relation in
this logic is defined in the standard manner: given a fuzzy ontology
$\mathcal{O}^{\mathbb{F}}$, we get that
$\mathcal{O}^{\mathbb{F}}\mathrel{\scalebox{1.0}[1.5]{$\shortmid$}\mkern-3.1mu\raisebox{0.43057pt}{$\approx$}}(C(a),n)$
iff $C^{\mathcal{I}}(a^{\mathcal{I}})\geq n$ in every fuzzy model
$\mathcal{I}$ of $\mathcal{O}^{\mathbb{F}}$. The general notions have later
been extended to consider also membership degrees in the TBox (?) and
reasoning tasks such as query answering (?, ?). In such a setting, ? (?)
showed that for DL-Lite and BCQs,
$\mathcal{O}^{\mathbb{F}}\mathrel{\scalebox{1.0}[1.5]{$\shortmid$}\mkern-3.1mu\raisebox{0.43057pt}{$\approx$}}\langle\alpha,n\rangle$
iff $\mathcal{O}_{\geq n}\models\alpha$ where $\mathcal{O}_{\geq n}$ is the
classical ontology—called the $n$-cut—containing only those axioms of
$\mathcal{O}^{\mathbb{F}}$ annotated with a degree greater or equal to $n$.
Hence, the next proposition and Theorem 19 by ? allow us to reduce BCQ (hence
also assertion) entailments over fuzzy DL-Lite ontologies to computation of
provenance in the fuzzy semiring.

######  Proposition 3.11.

If $\mathbb{F}$ is the _fuzzy semiring_ , then for every satisfiable annotated
${\cal E\\!LHI}_{\bot}$ ontology $\mathcal{O}^{\mathbb{F}}$ and $n\in[0,1]$:

  1. 1.

for every BCQ (or assertion) $\alpha$,
$\mathcal{P}(\alpha,\mathcal{O}^{\mathbb{F}})\geq n$ iff $\mathcal{O}_{\geq
n}\models\alpha$;

  2. 2.

if $\mathcal{O}^{\mathbb{F}}$ does not feature $\bot$, then for every GCI
between basic concepts $\alpha$,
$\mathcal{P}(\alpha,\mathcal{O}^{\mathbb{F}})\geq n$ iff $\mathcal{O}_{\geq
n}\models\alpha$.

Note that we cannot extend the proposition to GCIs when $\mathcal{O}$ features
$\bot$: If $\mathcal{O}^{\mathbb{F}}=\\{(A\sqsubseteq B,0.5),(A\sqsubseteq
C,0.5),(B\sqcap C\sqsubseteq\bot,0.9)\\}$, then $\mathcal{O}_{\geq
0.9}\not\models A\sqsubseteq D$ for every $D\in{\sf N_{C}}$ but
$\mathcal{P}(A\sqsubseteq D,\mathcal{O}^{\mathbb{F}})=1$ (cf. Remark 3.2).

These $n$-cuts are widely used in the fuzzy logic community. In the fuzzy DL
literature, it is more common to use a method called _crispification_ in which
different concept names are used in a classical interpretation to represent
the truth degrees assigned by a fuzzy interpretation (?, ?, ?). While
crispification allows for a more fine-grained semantic analysis in general, by
“cutting” also the interpretations at the desired degree $n$, one obtains an
interpretation which is a model of the $n$-cut whenever the fuzzy
interpretation is a model of the original ontology, thus preserving the
result.

##### Possibilistic DL

The case of possibilistic DL (?) is similar to the case of fuzzy DL. A
possibilistic ontology assigns a _possibility degree_ from the interval [0,1]
to each axiom in the ontology. The semantics is based on a possibility
distribution over all the possible interpretations $\mathcal{I}$, which
depends on the degrees of the axioms not satisfied by $\mathcal{I}$. Although
at first sight the semantics does not exactly fit our definition, it has been
shown that reasoning in $\min$-based possibilistic DLs (?, Section 3) can be
reduced to classical reasoning over so-called $n$-cuts (?), where the $n$-cut
$\mathcal{O}_{\geq n}$ of an ontology $\mathcal{O}$ is the (classical) sub-
ontology obtained considering only those axioms that are labelled with an
element greater or equal to $n$. In a nutshell, the possibility degree of a
consequence is at least $n$ iff it follows from its $n$-cut. To find a tight
possibility degree, we need to compute the maximum over such possible
ontologies. Hence, by Proposition 3.11, possibilistic reasoning can be reduced
to provenance computations over the fuzzy semiring. Note, however, that the
same is not true for product-based possibilistic semantics (?), as the
computation of $n$-cuts does not suffice—the product of values above $n$ can
yield degrees below $n$. Typically, possibilistic semantics target reasoning
with inconsistent ontologies and are based on an inconsistency degree, which
is obtained from combinations of axioms that are jointly inconsistent under
classical semantics. In possibilistic logics, this inconsistency is removed by
ignoring axioms excluded by the $n$-cut. In our case, the provenance of any
axiom over an inconsistent ontology is the sum of all the semiring elements,
so we restrict our comparison to the case of satisfiable ontologies.

##### Access Control

? (?) propose to annotate axioms in an ontology with a label belonging to a
so-called _access lattice_ $(L,\min,\max,\bot,\top)$ (cf. Example 2.3). The
label expresses the minimum rights that a user should have to access that
knowledge. Hence, consequences should only be visible to users that access to
sufficient axioms to derive them. The main reasoning task in this setting is
to compute the minimum rights required for a user to access a given
consequence. One of the main results of ? (?) shows that this problem is
equivalent to the computation of the provenance for the consequence over
$(L,\min,\max,\bot,\top)$. Specifically, recall that every distributive
lattice is a semiring where both operations (which correspond to the join and
meet of the lattice) are idempotent. Each ontology defines a lattice element
computed as the meet of the labels of its axioms. ? show that the access level
of a consequence $\alpha$ is equivalent to the join of the labels of all
subontologies that entail $\alpha$.

##### Bag semantics

When the ontology is annotated with elements of the counting semiring
(extended with $\infty$ to ensure $\omega$-continuity)
$\mathbb{N}=(\mathbb{N}\cup\\{\infty\\},+,\times,0,1)$, our semantics does not
coincide with the bag semantics for OBDA (?, ?) and showcases a counter-
intuitive behavior. Consider for example the annotated ontology
$\mathcal{O}^{\mathbb{N}}=\\{(A(a),2),(B(a),3),(A\sqsubseteq
C,1),(B\sqsubseteq C,1)\\}$ and let ${\mathcal{O}^{\mathbb{N}}}^{\prime}$ be
obtained from $\mathcal{O}^{\mathbb{N}}$ by changing the annotation of $A(a)$
to 3. The multiplicity of $C(a)$ in both $\mathcal{O}^{\mathbb{N}}$ and
${\mathcal{O}^{\mathbb{N}}}^{\prime}$ according to the bag semantics of ? is
$3$ while $\mathcal{P}(C(a),\mathcal{O}^{\mathbb{N}})=5$ (since every model
$\mathcal{I}$ of $\mathcal{O}^{\mathbb{N}}$ is such that
$\\{(a^{\mathcal{I}},2),(a^{\mathcal{I}},3)\\}\subseteq C^{\mathcal{I}}$), and
$\mathcal{P}(C(a),{\mathcal{O}^{\mathbb{N}}}^{\prime})=3$. We will see in
Section 3.5 that several issues indeed arise when the semiring is not
$\oplus$-idempotent, and will thus focus on the $\oplus$-idempotent case.

In the context of Datalog queries, ? (?) consider two alternative ways of
defining provenance semantics based on annotated models. The first one (called
annotated model-based semantics) is defined on a restricted class of semirings
where every set of semiring elements has a greatest lower bound and allows to
capture the bag semantics for OBDA when used with the counting semiring, while
the second one (called set-annotated model-based semantics) is similar to the
one we consider here (cf. Lemma 3.27). However, these two provenance semantics
for Datalog suffer from unexpected behaviors when $\oplus$ is not idempotent,
and they coincide in the case where $\oplus$ is idempotent. Hence, we do not
consider in this paper the alternative definition similar to the annotated
model-based semantics.

Note that replacing the counting semiring $\mathbb{N}$ by
$\mathbb{K}=(\mathbb{N},\max,\times,0,1)$ does not capture the bag semantics
for OBDA. While it would solve the problem mentioned earlier (we would have
$\mathcal{P}(C(a),\mathcal{O}^{\mathbb{N}})=\mathcal{P}(C(a),{\mathcal{O}^{\mathbb{N}}}^{\prime})=3$),
we would not be able to capture the bag semantics of conjunctive queries as
defined by ?: if $\mathcal{O}^{\mathbb{K}}=\\{(R(a,b),2),(R(a,c),3)\\}$,
$\mathcal{P}(\exists yR(a,y),\mathcal{O}^{\mathbb{K}})=3$ while its
multiplicity is 5 according to the bag semantics.

###  3.4 Canonical Model

Given an annotated ${\cal E\\!LHI}_{\bot}$ ontology $\mathcal{O}^{\mathbb{K}}$
that is satisfiable, we inductively define a canonical model
$\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}$ of $\mathcal{O}^{\mathbb{K}}$ as
follows. Let $\mathcal{I}_{0}$ be such that:

  * •

$\Delta^{\mathcal{I}_{0}}:={\sf N_{I}}$;

  * •

$a^{\mathcal{I}_{0}}:=a$, for all $a\in{\sf N_{I}}$;

  * •

$(a,\kappa)\in A^{\mathcal{I}_{0}}$ iff
$(A(a),\kappa)\in\mathcal{O}^{\mathbb{K}}$;

  * •

$(a,b,\kappa)\in R^{\mathcal{I}_{0}}$ iff
$(R(a,b),\kappa)\in\mathcal{O}^{\mathbb{K}}$.

Suppose $\mathcal{I}_{n}$ is defined. We define $\mathcal{I}_{n+1}$ by
choosing an axiom in $\mathcal{O}^{\mathbb{K}}$ and applying the corresponding
rule among the following.

  * •

If $({P\sqsubseteq Q},{\kappa})\in\mathcal{O}^{\mathbb{K}}$ and
$(d,e,\kappa^{\prime})\in P^{\mathcal{I}_{n}}$, then
$(d,e,\kappa\otimes\kappa^{\prime})\in Q^{\mathcal{I}_{n+1}}$.

  * •

If $({C\sqsubseteq A},{\kappa})\in\mathcal{O}^{\mathbb{K}}$ and
$(d,\kappa^{\prime})\in C^{\mathcal{I}_{n}}$, then
$(d,\kappa\otimes\kappa^{\prime})\in A^{\mathcal{I}_{n+1}}$.

  * •

If $({C\sqsubseteq\exists P},{\kappa})\in\mathcal{O}^{\mathbb{K}}$ and
$(d,\kappa^{\prime})\in C^{\mathcal{I}_{n}}$, then
$\Delta^{\mathcal{I}_{n+1}}:=\Delta^{\mathcal{I}_{n}}\cup\\{d_{f}\\}$ with
$d_{f}$ a fresh element, and $(d,d_{f},\kappa\otimes\kappa^{\prime})\in
P^{\mathcal{I}_{n+1}}$. Note that $P$ can be a role name or an inverse role.

We assume that rule application is fair, meaning that if a rule is applicable
at a certain place, it will eventually be applied there. We define
$\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}:=\bigcup_{n\geq 0}\mathcal{I}_{n}$.
Proposition 3.12 is an easy consequence of the definition of
$\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}$.

######  Proposition 3.12.

If $\mathcal{O}^{\mathbb{K}}$ is a satisfiable $\mathbb{K}$-annotated ${\cal
E\\!LHI}_{\bot}$ ontology then
$\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}\models\mathcal{O}^{\mathbb{K}}$.

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 and $d,e\in\Delta^{\mathcal{I}}$. A
_homomorphism_ $g:\mathcal{I}\rightarrow\mathcal{J}$ is a function from
$\Delta^{\mathcal{I}}$ to $\Delta^{\mathcal{J}}$ such that:

  * •

for all individual names $a\in{\sf N_{I}}$,
$g(a^{\mathcal{I}})=a^{\mathcal{J}}$;

  * •

for all concept names $A\in{\sf N_{C}}$, if $(d,\kappa)\in A^{\mathcal{I}}$
then $(g(d),\kappa)\in A^{\mathcal{J}}$;

  * •

for all role names $R\in{\sf N_{R}}$, if $(d,e,\kappa)\in R^{\mathcal{I}}$
then $(g(d),g(e),\kappa)\in R^{\mathcal{J}}$.

Lemma 3.13 states that $\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}$ has the usual
property of canonical models.

######  Lemma 3.13.

For every model $\mathcal{I}$ of a satisfiable $\mathcal{O}^{\mathbb{K}}$,
there is a homomorphism
$g:\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}\rightarrow\mathcal{I}$.

Theorem 3.14 states that the canonical model behaves as expected for annotated
assertions and BCQs entailment (note that annotated BCQs actually subsume
annotated assertions, so that the two first points are consequences of the
last one).

######  Theorem 3.14.

For every satisfiable $\mathbb{K}$-annotated ${\cal E\\!LHI}_{\bot}$ ontology
$\mathcal{O}^{\mathbb{K}}$ the following holds:

  * •

for every $\kappa\in K$, every $a\in{\sf ind}(\mathcal{O}^{\mathbb{K}})$, and
every ${\cal E\\!LHI}_{\bot}$ concept name $A$, we have that
$\mathcal{O}^{\mathbb{K}}\models(A(a),\kappa)$ iff
$\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}\models(A(a),\kappa)$;

  * •

for every $\kappa\in K$, every $a,b\in{\sf ind}(\mathcal{O}^{\mathbb{K}})$,
and every role name $R$, $\mathcal{O}^{\mathbb{K}}\models(R(a,b),\kappa)$ iff
$\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}\models(R(a,b),\kappa)$;

  * •

for every $\kappa\in K$, every BCQ $q$, we have that
$\mathcal{O}^{\mathbb{K}}\models(q,\kappa)$ iff
$\mathcal{I}_{\mathcal{O}^{\mathbb{K}}}\models(q,\kappa)$.

We now turn our attention to how GCIs entailment can be captured (or not)
using a canonical model. For a basic concept $C$ (i.e. a concept name $A$ or a
concept of the form $\exists P$), we define its canonical model
$\mathcal{I}_{C}$ as the interpretation with domain
$\Delta^{\mathcal{I}_{C}}:=\\{d_{C}\\}\cup{\sf N_{I}}$ if $C$ is a concept
name, and $\Delta^{\mathcal{I}_{C}}:=\\{d_{C},d_{f}\\}\cup{\sf N_{I}}$
otherwise, such that $a^{\mathcal{I}_{C}}:=a$ for all $a\in{\sf N_{I}}$,
$A^{\mathcal{I}_{C}}:=\\{(d_{A},\mathbb{1})\\}$ if $C=A\in{\sf N_{C}}$,
$R^{\mathcal{I}_{C}}:=\\{(d_{\exists R},d_{f},\mathbb{1})\\}$ if $C=\exists
R$, and $R^{\mathcal{I}_{C}}:=\\{(d_{f},d_{\exists R^{-}},\mathbb{1})\\}$ if
$C=\exists R^{-}$, and all other concept and role names are mapped to the
empty set. The canonical model $\mathcal{I}_{C,\mathcal{O}^{\mathbb{K}}}$ for
a basic concept $C$ and a $\mathbb{K}$-annotated ${\cal E\\!LHI}_{\bot}$
ontology $\mathcal{O}^{\mathbb{K}}$ is defined in the same way as the
canonical model for $\mathcal{O}^{\mathbb{K}}$ except that $\mathcal{I}_{0}$
starts with $\mathcal{I}_{C}$ (and assertions if they are present in the
ontology). Finally, given an annotation $\kappa\in K$, we define
$\mathcal{I}_{C,\kappa,\mathcal{O}^{\mathbb{K}}}$ in the same way as
$\mathcal{I}_{C,\mathcal{O}^{\mathbb{K}}}$ except that we use $\kappa$ instead
of $\mathbb{1}$ in the definition of $\mathcal{I}_{C}$.

######  Lemma 3.15.

Let $\mathcal{I}$ be a model of $\mathcal{O}^{\mathbb{K}}$ with $(d,\kappa)\in
C^{\mathcal{I}}$, where $C$ is a _basic_ concept. Then there exists a
homomorphism
$g:\mathcal{I}_{C,\kappa,\mathcal{O}^{\mathbb{K}}}\rightarrow\mathcal{I}$ such
that $g(d_{C})=d$.

Lemma 3.15 does not hold if $C$ is a complex ${\cal E\\!LHI}_{\bot}$ concept
(i.e., not basic). Example 3.16 illustrates a model $\mathcal{I}$ of
$\mathcal{O}^{\mathbb{K}}$ where $(d,\kappa)\in C^{\mathcal{I}}$, with
$C=A\sqcap B$, without a homomorphism satisfying the properties of Lemma 3.15
if we extend the definition of
$\mathcal{I}_{C,\kappa,\mathcal{O}^{\mathbb{K}}}$ to a complex concept in the
natural way.

######  Example 3.16.

Let $\mathcal{O}^{\mathbb{K}}=\\{(A\sqsubseteq D,\kappa^{\prime})\\}$ and
$B\in{\sf N_{C}}$ and consider the following model $\mathcal{I}$:

$\begin{array}[]{l@{\ }l@{\ }l@{\
}l}A^{\mathcal{I}}=\\{(e,\mathbb{1})\\},&B^{\mathcal{I}}=\\{(e,\kappa)\\},&D^{\mathcal{I}}=\\{(e,\kappa^{\prime})\\}\end{array}$

It is the case that $(A\sqcap B)^{\mathcal{I}}=\\{(e,\kappa)\\}$. However, if
we build $\mathcal{I}_{A\sqcap B,\kappa,\mathcal{O}^{\mathbb{K}}}$ in the
natural way:

$\displaystyle A^{\mathcal{I}_{A\sqcap
B,\kappa,\mathcal{O}^{\mathbb{K}}}}=\\{(d_{A\sqcap B},\kappa)\\},$
$\displaystyle\quad B^{\mathcal{I}_{A\sqcap
B,\kappa,\mathcal{O}^{\mathbb{K}}}}=\\{(d_{A\sqcap B},\kappa)\\},$
$\displaystyle D^{\mathcal{I}_{A\sqcap
B,\kappa,\mathcal{O}^{\mathbb{K}}}}=\\{(d_{A\sqcap
B},\kappa^{\prime}\otimes\kappa)\\},$

there is no homomorphism $g:\mathcal{I}_{A\sqcap
B,\kappa,\mathcal{O}^{\mathbb{K}}}\rightarrow\mathcal{I}$ such that
$g(d_{A\sqcap B})=e$ for $\kappa\neq\mathbb{1}$. ∎

We are now ready to state the result of this subsection for annotated GCIs;
yet, we need to restrict them to have only basic concepts, since the annotated
ontology from Example 3.16 is a counter-example the general case: it is easy
to check that $(d_{A\sqcap B},\kappa^{\prime})\in D^{\mathcal{I}_{A\sqcap
B,\mathcal{O}^{\mathbb{K}}}}$, but
$\mathcal{O}^{\mathbb{K}}\not\models(A\sqcap B\sqsubseteq D,\kappa^{\prime})$
because if we define $\mathcal{I}$ by $A^{\mathcal{I}}=\\{(e,\chi)\\}$,
$B^{\mathcal{I}}=\\{(e,\kappa)\\}$, and
$D^{\mathcal{I}}=\\{(e,\chi\otimes\kappa^{\prime})\\}$, then $\mathcal{I}$ is
a model of $\mathcal{O}^{\mathbb{K}}$ but $\mathcal{I}\not\models(A\sqcap
B\sqsubseteq D,\kappa^{\prime})$.

######  Theorem 3.17.

Assume $\mathbb{K}$ is a commutative $\otimes$-idempotent $\omega$-continuous
semiring. Let $\mathcal{O}^{\mathbb{K}}$ be a satisfiable
$\mathbb{K}$-annotated ${\cal E\\!LHI}_{\bot}$ ontology and let $C,D$ be
${\cal E\\!LHI}_{\bot}$ _basic_ concepts satisfiable w.r.t.
$\mathcal{O}^{\mathbb{K}}$ (meaning that the canonical model of
$\mathcal{O}^{\mathbb{K}}$ and $C$ exists). Then, for every $\kappa\in K$,
$(d_{C},\kappa)\in D^{\mathcal{I}_{C,\mathcal{O}^{\mathbb{K}}}}$ iff
${\mathcal{O}^{\mathbb{K}}}\models(C\sqsubseteq D,\kappa)$.

Example 3.18 shows that the $\otimes$-idempotency condition is necessary.

######  Example 3.18.

Let $\mathcal{O}^{\mathbb{K}}=\\{(A\sqsubseteq B_{1},\mathbb{1}),(A\sqsubseteq
B_{2},\mathbb{1}),(B_{1}\sqcap B_{2}\sqsubseteq C,\mathbb{1})\\}$. It is easy
to check that $(d_{A},\mathbb{1})\in
C^{\mathcal{I}_{A,\mathcal{O}^{\mathbb{K}}}}$. However,
${\mathcal{O}^{\mathbb{K}}}\not\models(A\sqsubseteq C,\mathbb{1})$ if
$\mathbb{K}$ is not $\otimes$-idempotent. Indeed, let $\epsilon\in K$ such
that $\epsilon\otimes\epsilon\neq\epsilon$, $\kappa\in K$ such that there is
no $\chi\in K$ such that $\kappa\otimes\chi=\kappa\otimes\kappa$ and
$\epsilon\otimes\chi=\epsilon\otimes\epsilon$, and let $\mathcal{I}$ be an
interpretation such that:

$\displaystyle A^{\mathcal{I}}=$
$\displaystyle\\{(e,\epsilon),(d,\kappa)\\}\quad
B_{1}^{\mathcal{I}}=\\{(e,\epsilon),(d,\kappa)\\}\quad
B_{2}^{\mathcal{I}}=\\{(e,\epsilon),(d,\kappa)\\}\quad
C^{\mathcal{I}}=\\{(e,\epsilon\otimes\epsilon)(d,\kappa\otimes\kappa)\\}.$

$\mathcal{I}$ is a model of $\mathcal{O}^{\mathbb{K}}$ and for every $\chi\in
K$, $\mathcal{I}\not\models(A\sqsubseteq C,\chi)$. In particular,
$\mathcal{I}\not\models(A\sqsubseteq C,\mathbb{1})$. ∎

The arguably counter-intuitive behaviour illustrated in Example 3.18 leads us
to the next subsection that studies properties of our semantics.

###  3.5 Properties on Idempotent Semirings

Inspired by Definition 3 and Properties 1 and 3 of ? (?), the theorems in this
subsection show that under some restrictions on the semirings, our semiring
provenance definition satisfies properties that are expected for a provenance
semantics.

##### Preservation of entailment

Theorem 3.19 ensures that the semantics reflects the entailment or non-
entailment of axioms and queries.

######  Theorem 3.19.

If $\mathbb{K}$ is a commutative $\otimes$-idempotent $\omega$-continuous
semiring then, for every $\mathbb{K}$-annotated ${\cal E\\!LHI}_{\bot}$
ontology $\mathcal{O}^{\mathbb{K}}=\langle\mathcal{O},\lambda\rangle$ and
every $\alpha$ that is an assertion, a BCQ, or a GCI between basic concepts:

  * •

$\mathcal{O}\not\models\alpha$ implies
$\mathcal{P}(\alpha,\mathcal{O}^{\mathbb{K}})=\mathbb{0}$, and

  * •

if $\mathbb{K}$ is positive and
$\mathcal{P}(\alpha,\mathcal{O}^{\mathbb{K}})=\mathbb{0}$ then
$\mathcal{O}\not\models\alpha$.

Unfortunately, Theorem 3.19 does not hold if $\alpha$ is a GCI with a complex
concept on its left-hand side, as we can see on Example 3.20.

######  Example 3.20.

Let $\mathbb{K}$ be a positive semiring,
$\mathcal{O}^{\mathbb{K}}=\\{(A\sqsubseteq D,\kappa^{\prime})\\}$ and
$B\in{\sf N_{C}}$. It holds that $\mathcal{O}\models A\sqcap B\sqsubseteq D$
but $\mathcal{P}(A\sqcap B\sqsubseteq D,\mathcal{O}^{\mathbb{K}})=\mathbb{0}$.
This can be checked using the following models of $\mathcal{O}^{\mathbb{K}}$,
assuming that $\kappa$ is such that
$\kappa^{\prime}\otimes\kappa\neq\kappa^{\prime}$:

$\begin{array}[]{l@{\ }l@{\ }l@{\
}l}A^{\mathcal{I}_{1}}=\\{(e,\kappa)\\},&B^{\mathcal{I}_{1}}=\\{(e,\mathbb{1})\\},&(A\sqcap
B)^{\mathcal{I}_{1}}=\\{(e,\kappa)\\},&D^{\mathcal{I}_{1}}=\\{(e,\kappa^{\prime}\otimes\kappa)\\}\\\
A^{\mathcal{I}_{2}}=\\{(e,\mathbb{1})\\},&B^{\mathcal{I}_{2}}=\\{(e,\kappa)\\},&(A\sqcap
B)^{\mathcal{I}_{2}}=\\{(e,\kappa)\\},&D^{\mathcal{I}_{2}}=\\{(e,\kappa^{\prime})\\}\end{array}\qed$

The next example illustrates the impact of $\otimes$-idempotency for the
${\cal E\\!L}$ family and shows that when the multiplication is not
idempotent, Theorem 3.19 does not hold.

######  Example 3.21.

Let $\mathbb{K}$ be a $\otimes$-idempotent semiring and consider the ontology

$\mathcal{O}^{\mathbb{K}}=\\{(A\sqsubseteq B_{1},\kappa_{1}),(A\sqsubseteq
B_{2},\kappa_{2}),(B_{1}\sqcap B_{2}\sqsubseteq C,\kappa_{3})\\}.$

If $\mathcal{I}$ is a model of $\mathcal{O}^{\mathbb{K}}$ and $(e,\epsilon)\in
A^{\mathcal{I}}$, then $(e,\epsilon\otimes\kappa_{1})\in B_{1}^{\mathcal{I}}$
and $(e,\epsilon\otimes\kappa_{2})\in B_{2}^{\mathcal{I}}$ so
$(e,\epsilon\otimes\kappa_{1}\otimes\epsilon\otimes\kappa_{2})\in(B_{1}\sqcap
B_{2})^{\mathcal{I}}$, i.e.
$(e,\epsilon\otimes\kappa_{1}\otimes\kappa_{2})\in(B_{1}\sqcap
B_{2})^{\mathcal{I}}$ by $\otimes$-idempotency, which implies
$(e,\epsilon\otimes\kappa_{1}\otimes\kappa_{2}\otimes\kappa_{3})\in
C^{\mathcal{I}}$. Thus we get that
$\mathcal{O}^{\mathbb{K}}\models(A\sqsubseteq
C,\kappa_{1}\otimes\kappa_{2}\otimes\kappa_{3})$ and $\mathcal{P}(A\sqsubseteq
C,\mathcal{O}^{\mathbb{K}})=\kappa_{1}\otimes\kappa_{2}\otimes\kappa_{3}$.

This intuitive behavior is lost if $\mathbb{K}$ is not $\otimes$-idempotent.
Indeed, we have seen in Example 3.18 that in this case, even if we set
$\kappa_{1}=\kappa_{2}=\kappa_{3}=\mathbb{1}$,
$\mathcal{O}^{\mathbb{K}}\not\models(A\sqsubseteq C,\chi)$ for every $\chi\in
K$. Hence $\mathcal{P}(A\sqsubseteq C,\mathcal{O}^{\mathbb{K}})=\mathbb{0}$. ∎

Requiring $\otimes$-idempotency amounts to neglecting the number of times an
axiom is used in a derivation. Consider the ontology
$\mathcal{O}^{\mathbb{N}^{\infty}\llbracket{\sf
X}\rrbracket}=\mathcal{O}^{\sf{Trio}[{\sf X}]}=\\{(A\sqsubseteq
B,x_{1}),(B\sqsubseteq A,x_{2})\\}$. In the non-idempotent
$\mathbb{N}^{\infty}\llbracket{\sf X}\rrbracket$ semiring,
$\mathcal{P}(A\sqsubseteq B,\mathcal{O}^{\mathbb{N}^{\infty}\llbracket{\sf
X}\rrbracket})=\sum_{n\geq 0}x_{1}(x_{1}x_{2})^{n}$, while in the
$\otimes$-idempotent $\sf{Trio}[{\sf X}]$ semiring $\mathcal{P}(A\sqsubseteq
B,\mathcal{O}^{\sf{Trio}[{\sf X}]})=x_{1}+x_{1}x_{2}$.

In Sections 4 and 5, we will focus on $\otimes$-idempotent semirings because
we are interested in computing provenance not only for assertions or queries,
but also for GCIs. In particular, when a non-annotated ontology entails the
GCI $C\sqsubseteq D$, with $C,D$ basic concepts, we want the annotated version
of the ontology to entail $(C\sqsubseteq D,\kappa)$ for some semiring element
$\kappa$, as guaranteed by Theorem 3.19. The non-idempotent case could be
relevant when one is not concerned with provenance for GCI entailment, and is
left as future work.

##### Consistency with semiring provenance for positive relational algebra
queries

Theorems 3.22 and 3.24 ensure that our notion of provenance is consistent with
the one defined for relational algebra queries over annotated databases. Given
an annotated set of facts
$\mathcal{D}^{\mathbb{K}}=\langle\mathcal{D},\lambda\rangle$ and a Boolean UCQ
$q=\exists\vec{x}\bigvee_{i=1}^{n}\varphi_{i}(\vec{x})$, we denote the
relational provenance of $q$ over $\mathcal{D}^{\mathbb{K}}$ seen as an
annotated database by

$\mathcal{P}_{DB}(q,\mathcal{D}^{\mathbb{K}})=\bigoplus_{i=1}^{n}\bigoplus_{\pi\in\Pi(\varphi_{i},\mathcal{D})}\bigotimes_{P(\vec{t})\in\varphi_{i}}\lambda(\pi(P(\vec{t}))),$

where $\Pi(\varphi_{i},\mathcal{D})$ is the set of matches of $\varphi_{i}$ in
$\mathcal{D}$ (?).

######  Theorem 3.22.

If $\mathbb{K}$ is a commutative $\oplus$-idempotent $\omega$-continuous
semiring, then for every $\mathbb{K}$-annotated ontology
$\mathcal{O}^{\mathbb{K}}=\langle\mathcal{O},\lambda\rangle$ containing only
assertions, and every BCQ $q$, $\mathcal{P}(q,\mathcal{O}^{\mathbb{K}})$ is
equal to the relational provenance of $q$ over $\mathcal{O}^{\mathbb{K}}$ seen
as an annotated database.

Example 3.23 shows that $\oplus$-idempotency is a necessary condition of
Theorem 3.22.

######  Example 3.23.

Let $\mathbb{K}$ be a semiring which is not $\oplus$-idempotent and $\kappa\in
K$ such that $\kappa\oplus\kappa\neq\kappa$. Let
$\mathcal{O}^{\mathbb{K}}=\\{(R(a,b),\kappa),(R(a,c),\kappa)\\}$ and
$q=\exists y\,R(a,y)$. For every model $\mathcal{I}$ of
$\mathcal{O}^{\mathbb{K}}$, there are the following matches for the extended
version $\boldsymbol{q}=\exists yt\,R(a,y,t)$ of $q$ in $\mathcal{I}$:
$\pi_{1}(y)=b$ and $\pi_{1}(t)=\kappa$, and $\pi_{2}(y)=b$ and
$\pi_{2}(t)=\kappa$, and there exists a model where these are the only
matches. Hence $\bigcap_{\mathcal{I}\models\mathcal{O}^{\mathbb{K}}}{\sf
prov}_{\mathcal{I}}({\boldsymbol{q}})=\\{\kappa\\}$ and
$\mathcal{P}(q,\mathcal{O}^{\mathbb{K}})=\kappa$, which is different from the
relational provenance of $q$ over $\mathcal{O}^{\mathbb{K}}$,
$\mathcal{P}_{DB}(q,\mathcal{O}^{\mathbb{K}})=\kappa\oplus\kappa$.

Theorem 3.22 does not hold when $\oplus$ is not idempotent even if all
assertions have distinct annotations. Consider $\mathcal{O}^{\mathbb{N}[{\sf
X}]}=\\{(R(a,b),x_{1}),(R(a,c),x_{2})\\}$ and $q=\exists yz\,R(a,y)\land
R(a,z)$. Then we get $\mathcal{P}(q,\mathcal{O}^{\mathbb{N}[{\sf
X}]})=x_{1}^{2}+x_{2}^{2}+x_{1}x_{2}$ while
$\mathcal{P}_{DB}(q,\mathcal{O}^{\mathbb{N}[{\sf
X}]})=x_{1}^{2}+x_{2}^{2}+\mathbf{2}x_{1}x_{2}$. Our notion of provenance does
not distinguish between the match that maps $y$ to $b$ and $z$ to $c$ and the
one that maps $y$ to $c$ and $z$ to $b$. ∎

The following theorem extends the result of Theorem 3.22 to the case of atomic
queries where the ontology is allowed to have a restricted form of GCIs. The
intuition behind the theorem is that one can rewrite atomic queries into UCQs
by unfolding the wanted concept name into the prerequisites for deriving it.

######  Theorem 3.24.

Let $\mathbb{K}$ be a commutative $\oplus$-idempotent $\omega$-continuous
semiring, and $A$ a fixed (but arbitrary) concept name. For every
$\mathbb{K}$-annotated ontology
$\mathcal{O}^{\mathbb{K}}=\langle\mathcal{O},\lambda\rangle$ that contains
only (i) assertions and (ii) GCIs of the form $C\sqsubseteq A$, labelled with
$\mathbb{1}$, where $C$ is an ${\cal E\\!LHI}$ concept not containing $A$, and
every $a\in{\sf N_{I}}$, $\mathcal{P}(A(a),\mathcal{O}^{\mathbb{K}})$ equals
the relational provenance of the query

$q:=A(a)\vee\bigvee_{C\sqsubseteq A\in\mathcal{O}}q_{C}(a),$

where $q_{C}(x)$ is the rooted tree-shaped query that retrieves all instances
of $C$, over $\mathcal{O}^{\mathbb{K}}$ seen as an annotated database
(ignoring GCIs).

######  Remark 3.25.

Importantly, Theorem 3.24 does not hold if we replace the strong restriction
on the form of GCIs by the UCQ rewritability of $A(a)$ w.r.t. $\mathcal{O}$.
Indeed, consider the following case:
$\mathcal{O}^{\mathbb{K}}=\\{(B(a),\kappa),(B\sqsubseteq\exists
R,\mathbb{1}),(R\sqsubseteq S,\mathbb{1}),(\exists R\sqcap\exists S\sqsubseteq
A,\mathbb{1})\\}$. The UCQ rewriting of $A(a)$ w.r.t. $\mathcal{O}$ is
$A(a)\vee\exists y,z(R(a,y)\wedge S(a,z))\vee\exists y,z(R(a,y)\wedge
R(a,z))\vee B(a)$, hence its relational provenance is $\kappa$. However,
$\mathcal{P}(A(a),\mathcal{O}^{\mathbb{K}})=\kappa\otimes\kappa$.

##### Consistency with semiring provenance for Datalog queries

Theorem 3.26 ensures that our notion of provenance is also consistent with the
one defined for Datalog queries over annotated databases (?). Following the
notation of ? (?), given an annotated database
$\mathcal{D}^{\mathbb{K}}=\langle\mathcal{D},\lambda\rangle$ and Datalog
progam $\Sigma$, we denote the Datalog provenance of a fact $\alpha$ w.r.t.
$\Sigma$ and $\mathcal{D}^{\mathbb{K}}$ by

$\mathcal{P}_{Dat}(\Sigma,\mathcal{D}^{\mathbb{K}},\alpha)=\bigoplus_{t\in
T^{\Sigma}_{\mathcal{D}}(\alpha)}\ \bigotimes_{v\text{ is a leaf of
$t$}}\lambda(v)$

where $T^{\Sigma}_{\mathcal{D}}(\alpha)$ is the set of all derivation trees
for $\alpha$ w.r.t. $\Sigma$ and $\mathcal{D}$.

######  Theorem 3.26.

For each ${\cal E\\!LHI}$ concept $C$, let $q_{C}(x)$ be the rooted tree-
shaped CQ that corresponds to $C$, and for every GCI or RI $\alpha$, let
$F_{\alpha}$ be a nullary predicate.

If $\mathbb{K}$ is a commutative $\oplus$-idempotent $\omega$-continuous
semiring, then for every $\mathbb{K}$-annotated ontology
$\mathcal{O}^{\mathbb{K}}=\langle\mathcal{O},\lambda\rangle$ whose GCIs have
only concept names has right-hand sides and RIs are positive, for every BCQ
$q$, $\mathcal{P}(q,\mathcal{O}^{\mathbb{K}})$ is equal to the Datalog
provenance $\mathcal{P}_{Dat}(\Sigma,\mathcal{D}^{\mathbb{K}},\mathsf{goal})$
of $\mathsf{goal}$ w.r.t. $\Sigma$ and
$\mathcal{D}^{\mathbb{K}}=\langle\mathcal{D},\lambda^{\prime}\rangle$ with

$\displaystyle\Sigma=\\{q_{C}(x)\wedge F_{C\sqsubseteq A}\rightarrow A(x)\mid
C\sqsubseteq A\in\mathcal{O}\\}$ $\displaystyle\quad\quad\cup\\{P(x,y)\wedge
F_{P\sqsubseteq Q}\rightarrow Q(x,y)\mid P\sqsubseteq Q\in\mathcal{O}\\}$
$\displaystyle\quad\quad\cup\\{q\rightarrow\mathsf{goal}\\}$
$\displaystyle\mathcal{D}=\\{A(a)\mid A(a)\in\mathcal{O}\\}\cup\\{R(a,b)\mid
R(a,b)\in\mathcal{O}\\}\cup\\{F_{\alpha}\mid\alpha\text{ is a GCI or RI of
}\mathcal{O}\\}$ and
$\displaystyle\lambda^{\prime}(\alpha)=\lambda(\alpha)\text{ if }\alpha\text{
is an assertion of }\mathcal{O}$
$\displaystyle\lambda^{\prime}(F_{\alpha})=\lambda(\alpha)\text{ if
}\alpha\text{ is a GCI or RI of }\mathcal{O}.$

We show Theorem 3.26 using Proposition 3 of ? (?) which states that when
$\mathbb{K}$ is $\oplus$-idempotent,
$\mathcal{P}_{Dat}(\Sigma,\mathcal{D}^{\mathbb{K}},\mathsf{goal})=\mathcal{P}_{Dat}^{\texttt{SAM}}(\Sigma,\mathcal{D}^{\mathbb{K}},\mathsf{goal})$
where $\mathcal{P}_{Dat}^{\texttt{SAM}}$ is an alternative notion of
provenance semantics for Datalog (called set-annotated model-based provenance
semantics) defined as follows.
$\mathcal{P}_{Dat}^{\texttt{SAM}}(\Sigma,\mathcal{D}^{\mathbb{K}},\mathsf{goal})=\bigoplus_{\kappa\in\bigcap_{(I,\mu^{I})\models(\Sigma,\mathcal{D}^{\mathbb{K}})}\mu^{I}(\mathsf{goal})}\kappa,$
where $(I,\mu^{I})$ with $I$ a set of facts and $\mu^{I}$ a function from $I$
to the power-set of $K$ are such that
$(I,\mu^{I})\models(\Sigma,\mathcal{D}^{\mathbb{K}})$ if

  1. 1.

$\mathcal{D}\subseteq I$, and for every $\alpha\in\mathcal{D}$,
$\lambda^{\prime}(\alpha)\in\mu^{I}(\alpha)$;

  2. 2.

for every $\phi(\vec{x},\vec{y})\rightarrow H(\vec{x})$ in $\Sigma$, whenever
there is a homomorphism $h:\phi(\vec{x},\vec{y})\mapsto I$, then
$h(H(\vec{x}))\in I$ and if
$h(\phi(\vec{x},\vec{y}))=\beta_{1}\wedge\dots\wedge\beta_{n}$,
$\\{\bigotimes_{i=1}^{n}\kappa_{i}\mid(\kappa_{1},\dots,\kappa_{n})\in\mu^{I}(\beta_{1})\times\dots\times\mu^{I}(\beta_{n})\\}\subseteq\mu^{I}(h(H(\vec{x})))$.

Theorem 3.26 is thus a direct consequence of the following lemma, which shows
the correspondance between our provenance semantics and the set-annotated
model-based Datalog provenance semantics (note that the semiring is not
required to be $\oplus$-idempotent here).

######  Lemma 3.27.

If $\mathbb{K}$ is a commutative $\omega$-continuous semiring, then for every
$\mathbb{K}$-annotated ontology
$\mathcal{O}^{\mathbb{K}}=\langle\mathcal{O},\lambda\rangle$ whose GCIs have
only concept names has right-hand sides and RIs are positive, for every BCQ
$q$,
$\mathcal{P}(q,\mathcal{O}^{\mathbb{K}})=\mathcal{P}_{Dat}^{\texttt{SAM}}(\Sigma,\mathcal{D}^{\mathbb{K}},\mathsf{goal})$
where $\Sigma$ and $\mathcal{D}^{\mathbb{K}}$ are defined as in Theorem 3.26.

Since the Datalog provenance of a CQ seen as a Datalog query coincides with
its relational provenance, Example 3.23 shows that contrary to Lemma 3.27,
Theorem 3.26 does not hold when the addition is not idempotent.

##### Commutation with homomorphisms

Theorem 3.28 ensures that the provenance expression computed in a provenance
semiring can be used to compute the provenance value in any application
semiring to which it specializes correctly.

######  Theorem 3.28.

Let $\mathbb{K}_{1}$ and $\mathbb{K}_{2}$ be commutative $\omega$-continuous
semirings such that there is a $\omega$-continuous semiring homomorphism $h$
from $\mathbb{K}_{1}$ to $\mathbb{K}_{2}$. For every satisfiable ${\cal
E\\!LHI}_{\bot}$ ontology $\mathcal{O}$ and 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$, the
following holds.

  * •

If $\mathbb{K}_{1}$ and $\mathbb{K}_{2}$ are $\oplus$-idempotent then, for
every assertion or BCQ $\alpha$, we have that
$h(\mathcal{P}(\alpha,\mathcal{O}^{\mathbb{K}_{1}}))=\mathcal{P}(\alpha,\mathcal{O}^{\mathbb{K}_{2}})$.

  * •

If $\mathbb{K}_{1}$ and $\mathbb{K}_{2}$ are $\oplus$-idempotent and
$\otimes$-idempotent then, for every GCI $\alpha$ between basic concepts
satisfiable w.r.t. $\mathcal{O}$, we have that
$h(\mathcal{P}(\alpha,\mathcal{O}^{\mathbb{K}_{1}}))=\mathcal{P}(\alpha,\mathcal{O}^{\mathbb{K}_{2}})$.

Note that Theorem 3.28 does not hold if $\mathcal{O}$ is unsatisfiable: if
$\mathbb{K}_{1}=\sf{PosBool}[{\sf X}]$, $\mathbb{K}_{2}=\mathbb{F}$ is the
fuzzy semiring, and $h$ is the unique semiring homomorphism defined by
$h(x)=0.5$ for every $x\in{\sf X}$, then
$h(\mathcal{P}(\alpha,\mathcal{O}^{\mathbb{K}_{1}}))=h(\bigoplus_{x\in{\sf
X}}x)=0.5$ while
$\mathcal{P}(\alpha,\mathcal{O}^{\mathbb{K}_{2}})=\max_{n\in[0,1]}(n)=1$.

Example 3.29 shows that Theorem 3.28 does not hold without the assumption that
the addition is idempotent, even for simple ontologies with only concept name
inclusions.

######  Example 3.29.

Let $\mathbb{K}$ be a semiring which is not $\oplus$-idempotent and $\kappa\in
K$ such that $\kappa\oplus\kappa\neq\kappa$. Let

$\displaystyle\mathcal{O}=$ $\displaystyle\\{A(a),B(a),A\sqsubseteq
C,B\sqsubseteq C\\}$ $\displaystyle\mathcal{O}^{\mathbb{N}[{\sf X}]}=$
$\displaystyle\\{(A(a),x),(B(a),y),(A\sqsubseteq C,u),(B\sqsubseteq C,v)\\}$
$\displaystyle\mathcal{O}^{\mathbb{K}}=$
$\displaystyle\\{(A(a),\kappa),(B(a),\kappa),(A\sqsubseteq
C,\mathbb{1}),(B\sqsubseteq C,\mathbb{1})\\}.$

The provenance of $C(a)$ w.r.t. $\mathcal{O}^{\mathbb{N}[{\sf X}]}$ is
$\mathcal{P}(C(a),\mathcal{O}^{\mathbb{N}[{\sf X}]})=xu+yv$, hence, if we
consider the semiring homomorphism $h$ such that $h(x)=h(y)=\kappa$ and
$h(u)=h(v)=\mathbb{1}$, $h(\mathcal{P}(C(a),\mathcal{O}^{\mathbb{N}[{\sf
X}]}))=\kappa\oplus\kappa$. However,
$\mathcal{P}(C(a),\mathcal{O}^{\mathbb{K}})=\kappa$ since there exists a model
$\mathcal{I}$ of $\mathcal{O}^{\mathbb{K}}$ such that
$C^{\mathcal{I}}=\\{(a^{\mathcal{I}},\kappa)\\}$. Hence
$h(\mathcal{P}(C(a),\mathcal{O}^{\mathbb{N}[{\sf
X}]}))\neq\mathcal{P}(C(a),\mathcal{O}^{\mathbb{K}})$. ∎

The following example, that uses the same ontology as Example 3.21, shows why
the assumption that $\mathbb{K}_{1}$ is $\otimes$-idempotent is necessary for
the case of GCIs in Theorem 3.28.

######  Example 3.30.

Let $\mathcal{O}^{\mathbb{B}\llbracket{\sf
X}\rrbracket}=\mathcal{O}^{\sf{Why}[{\sf X}]}=\\{(A\sqsubseteq
B_{1},x),(A\sqsubseteq B_{2},y),(B_{1}\sqcap B_{2}\sqsubseteq C,z)\\}$ (recall
that $\mathbb{B}\llbracket{\sf X}\rrbracket$ and $\sf{Why}[{\sf X}]$ are both
$\oplus$-idempotent but only $\sf{Why}[{\sf X}]$ is $\otimes$-idempotent) and
$h:\mathbb{B}\llbracket{\sf X}\rrbracket\rightarrow\sf{Why}[{\sf X}]$ be the
identity over variables. It is easy to verify that $h$ is a semiring
homomorphism. As in Example 3.21, we obtain $\mathcal{P}(A\sqsubseteq
C,\mathcal{O}^{\mathbb{B}\llbracket{\sf X}\rrbracket})=0$ because
$\mathbb{B}\llbracket{\sf X}\rrbracket$ is not $\otimes$-idempotent. However,
we get that $\mathcal{P}(A\sqsubseteq C,\mathcal{O}^{\sf{Why}[{\sf X}]})=xyz$,
and hence $h(\mathcal{P}(A\sqsubseteq C,\mathcal{O}^{\mathbb{B}\llbracket{\sf
X}\rrbracket}))\neq\mathcal{P}(A\sqsubseteq C,\mathcal{O}^{\sf{Why}[{\sf
X}]})$. ∎

###  3.6 Discussion on Syntactic Restrictions

We conclude this section by explaining the restrictions on the form of the
right-hand side of the ${\cal E\\!LHI}_{\bot}$ GCIs. Example 3.31 illustrates
that when a conjunction occurs on the right-hand side of a GCI, Theorem 3.19
does not hold. Qualified role restrictions lead to the same kind of behavior
(they can be seen as implicit conjunctions).

######  Example 3.31.

Let $\mathcal{O}^{\mathbb{K}}=\\{(A\sqsubseteq B\sqcap
C,\kappa),(A(a),\kappa^{\prime})\\}$. All the following interpretations which
interpret $a$ by itself are models of $\mathcal{O}^{\mathbb{K}}$:

$\begin{array}[]{l@{\ }l@{\ }l}A^{\mathcal{I}_{1}}=\\{(a,\kappa)\\},&\quad
B^{\mathcal{I}_{1}}=\\{(a,\kappa\otimes\kappa^{\prime})\\},&C^{\mathcal{I}_{1}}=\\{(a,\kappa\otimes\kappa^{\prime})\\}\\\
A^{\mathcal{I}_{2}}=\\{(a,\kappa)\\},&\quad
B^{\mathcal{I}_{2}}=\\{(a,\kappa)\\},&C^{\mathcal{I}_{2}}=\\{(a,\kappa^{\prime})\\}\\\
A^{\mathcal{I}_{3}}=\\{(a,\kappa)\\},&\quad
B^{\mathcal{I}_{3}}=\\{(a,\mathbb{1})\\},&C^{\mathcal{I}_{3}}=\\{(a,\kappa\otimes\kappa^{\prime})\\}\end{array}$

Since the semantics does not provide a unique way to “split” the semiring
element $\kappa\otimes\kappa^{\prime}$ between the two elements of the
conjunction, if $\kappa\neq\mathbb{1}$ or $\kappa^{\prime}\neq\mathbb{1}$,
then $\mathcal{O}^{\mathbb{K}}\not\models(B(a),\chi)$ for any $\chi\in K$,
i.e. $\mathcal{P}(B(a),\mathcal{O}^{\mathbb{K}})=\mathbb{0}$. In particular,
$\mathcal{O}^{\mathbb{K}}\not\models(B(a),\kappa\otimes\kappa^{\prime})$ which
is arguably counter-intuitive since we intuitively know that $a$ is in $A$
with provenance $\kappa^{\prime}$ and that $A$ is a subclass of the
intersection of $B$ and $C$ with provenance $\kappa$. ∎

Partially normalizing the ontology before annotating it, or more specifically,
replacing e.g. annotated GCIs of the form $(C\sqsubseteq C_{1}\sqcap
C_{2},\kappa)$ by $(C\sqsubseteq C_{1},\kappa)$ and $(C\sqsubseteq
C_{2},\kappa)$, may be acceptable in most cases, even if the rewritten
ontology leads to additional—arguably natural—consequences compared to the
original one. For instance, even if
$\mathcal{O}^{\mathbb{K}}\not\models(A\sqsubseteq B,\kappa)$ in Example 3.31,
in many cases a user would accept to change the GCI of
$\mathcal{O}^{\mathbb{K}}$ to $(A\sqsubseteq B,\kappa)$ and $(A\sqsubseteq
C,\kappa)$ as it may reflect the original intention of the GCI since
$\\{A\sqsubseteq B,A\sqsubseteq C\\}$ and $A\sqsubseteq B\sqcap C$ are
semantically equivalent.

One could argue that it would be better to define the semantics so that only
$\mathcal{I}_{1}$ was a model of $\mathcal{O}^{\mathbb{K}}$ in Example 3.31,
instead of restricting the language as we do. We explain next why this is not
so simple.

One possibility is to change the definition of satisfaction of a GCI by an
interpretation such that $\mathcal{I}\models(A\sqsubseteq B\sqcap C,\kappa)$
iff for every $(d,\kappa^{\prime})\in A^{\mathcal{I}}$, then
$(d,\kappa\otimes\kappa^{\prime})\in B^{\mathcal{I}}$ and
$(d,\kappa\otimes\kappa^{\prime})\in C^{\mathcal{I}}$, and similarly for
qualified role restrictions. This approach leads to a counter-intuitive
behavior. For instance if $\mathcal{O}^{\mathbb{K}}=\emptyset$, then
$\mathcal{O}^{\mathbb{K}}\not\models(A\sqcap B\sqsubseteq A\sqcap
B,\mathbb{1})$, since there is a model $\mathcal{I}$ of
$\mathcal{O}^{\mathbb{K}}$ such that $A^{\mathcal{I}}=\\{(a,\kappa)\\}$ and
$B^{\mathcal{I}}=\\{(a,\kappa^{\prime})\\}$, so that $(A\sqcap
B)^{\mathcal{I}}=\\{(a,\kappa\otimes\kappa^{\prime})\\}$, and
$(a,\kappa\otimes\kappa^{\prime})\notin A^{\mathcal{I}}$,
$(a,\kappa\otimes\kappa^{\prime})\notin B^{\mathcal{I}}$. In contrast, our
definition of satisfaction ensures that for every interpretation $\mathcal{I}$
and concept $C$, $\mathcal{I}\models(C\sqsubseteq C,\mathbb{1})$.

Another possibility is to modify the interpretation of conjunctions and
qualified role restrictions such that

$\displaystyle(C\sqcap D)^{\mathcal{I}}$
$\displaystyle{}=\\{(d,\kappa)\mid(d,\kappa)\in C^{\mathcal{I}},(d,\kappa)\in
D^{\mathcal{I}}\\}$ and $\displaystyle(\exists R.C)^{\mathcal{I}}$
$\displaystyle{}=\\{(d,\kappa)\mid\exists e\in\Delta^{\mathcal{I}}\text{ s.t.
}(d,e,\kappa)\in R^{\mathcal{I}},(e,\kappa)\in C^{\mathcal{I}}\\}.$

However, this would lead to the loss of many natural and wanted entailments,
for example $\\{(A(a),\kappa),(B(a),\kappa^{\prime}),(A\sqcap B\sqsubseteq
C,\mathbb{1})\\}\not\models(C(a),\kappa\otimes\kappa^{\prime})$, and Theorem
3.19 would not hold.

Hence, restricting the syntax to prevent conjunctions on the right and
defining the semantics as usual in DLs seems to be the most natural way of
handling provenance in DL languages with conjunction. Since ${\cal E\\!L}$
ontologies are often already expressed in normal form, the main restriction in
our language is the avoidance of qualified existential restrictions on the
right-hand side.

##  4 Computing Provenance in the $\sf{Why}[{\sf X}]$ Semiring

We have seen in Section 3.5 that the most general case where the provenance
semantics have good properties is when the semiring is both $\oplus$\- and
$\otimes$-idempotent. By Theorem 3.28 and the fact that the provenance
semiring $\sf{Why}[{\sf X}]$ is universal for semirings which are $\oplus$\-
and $\otimes$-idempotent, it holds that for every semiring $\mathbb{K}$ with
these properties, every satisfiable $\mathbb{K}$-annotated ontology
$\mathcal{O}^{\mathbb{K}}=\langle\mathcal{O},\lambda\rangle$, and every axiom
or BCQ $\alpha$, the provenance $\mathcal{P}(\alpha,\mathcal{O}^{\mathbb{K}})$
can be computed by computing $\mathcal{P}(\alpha,\mathcal{O}^{\sf{Why}[{\sf
X}]})$ where $\mathcal{O}^{\sf{Why}[{\sf X}]}=\langle\mathcal{O},\lambda_{\sf
X}\rangle$ with $\lambda_{\sf X}$ an injective function from the axioms in
$\mathcal{O}$ to the set of variables ${\sf X}$, and evaluating the obtained
polynomial through the unique semiring homomorphism $h$ from $\sf{Why}[{\sf
X}]$ to $\mathbb{K}$ such that $h(\lambda_{\sf X}(\beta))=\lambda(\beta)$ for
every $\beta\in\mathcal{O}$. Hence, in this section, we focus on computing the
why-provenance $\mathcal{P}(\alpha,\mathcal{O}^{\sf{Why}[{\sf X}]})$.

Since we always consider $\sf{Why}[{\sf X}]$-annotated ontologies, we often
omit the superscript $\sf{Why}[{\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}$. We start with a general
proposition that shows that we can focus on _monomials_ , i.e. products of
variables, to compute why-provenance.

######  Proposition 4.1.

Let $\mathcal{O}$ be a satisfiable $\sf{Why}[{\sf X}]$-annotated ${\cal
E\\!LHI}_{\bot}$ ontology and $m$ be an element of $\sf{Why}[{\sf X}]$. If
$\mathcal{O}\models(\alpha,m)$ where $\alpha$ is a BCQ or an axiom that is not
a concept or role inclusion whose left-hand side is unsatisfiable w.r.t.
$\mathcal{O}$, then $m$ is a monomial over ${\sf X}$.

We can thus compute $\mathcal{P}(\alpha,\mathcal{O})$ by finding all monomials
$m$ over ${\sf X}$ such that $\mathcal{O}\models(\alpha,m)$.

######  Remark 4.2.

The condition on concept and role inclusions in Proposition 4.1 is due to the
fact that for GCI or role inclusion with an unsatisfiable left-hand side,
$\mathcal{O}^{\sf{Why}[{\sf X}]}\models(\alpha,\kappa)$ for every
$\kappa\in\sf{Why}[{\sf X}]$ (cf. Remark 3.2).

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

In this subsection, we present a completion algorithm for deriving annotated
axiom entailments from a $\sf{Why}[{\sf X}]$-annotated ${\cal E\\!LHI}_{\bot}$
ontology.

####  4.1.1 Normalization and Reduction to Annotated Assertion Entailment

As usual with completion algorithms, we restrict to ontologies in normal form.
An annotated ${\cal E\\!LHI}_{\bot}$ ontology $\mathcal{O}$ is in _normal
form_ if for every GCI $(\alpha,v)\in\mathcal{O}$, $\alpha$ is of the form

$A\sqsubseteq B,\ A\sqcap A^{\prime}\sqsubseteq B,\ A\sqsubseteq\exists R,\
A\sqsubseteq\exists R^{-},\ \exists R.A\sqsubseteq B,\text{ or }\exists
R^{-}.A\sqsubseteq B$

with $A,A^{\prime}\in{\sf N_{C}}\cup\\{\top\\}$, $B\in{\sf
N_{C}}\cup\\{\bot\\}$. Every $\sf{Why}[{\sf X}]$-annotated ${\cal
E\\!LHI}_{\bot}$ ontology can be transformed, in polynomial time, into an
ontology in normal form which entails the same $\sf{Why}[{\sf X}]$-annotated
axioms over the ontology signature, using the following rules where
$\widehat{C},\widehat{D}\notin{\sf N_{C}}\cup\\{\top\\}$ and $A$ is a fresh
concept name:

$\begin{array}[]{l@{\ }r@{\ }l@{\
}l}\mathsf{NF}_{1}:&(C\sqcap\widehat{D}\sqsubseteq
E,\,v)&\longrightarrow&(\widehat{D}\sqsubseteq A,\,1),(C\sqcap A\sqsubseteq
E,\,v)\\\ \mathsf{NF}_{2}:&(\exists P.\widehat{C}\sqsubseteq
D,\,v)&\longrightarrow&(\widehat{C}\sqsubseteq A,\,1),(\exists P.A\sqsubseteq
D,\,v)\\\ \mathsf{NF}_{3}:&(\widehat{C}\sqsubseteq\exists
P,\,v)&\longrightarrow&(\widehat{C}\sqsubseteq A,\,1),(A\sqsubseteq\exists
P,\,v).\end{array}$

######  Theorem 4.3.

Let $\mathcal{O}$ be a $\sf{Why}[{\sf X}]$-annotated ${\cal E\\!LHI}_{\bot}$
ontology, $\alpha$ an axiom, and $m$ a monomial over ${\sf X}$. Let
$\mathcal{O}^{\prime}$ be obtained by applying exhaustively Rules
$\mathsf{NF}_{1}$-$\mathsf{NF}_{3}$ to $\mathcal{O}$.

  * •

If $\mathcal{O}\models(\alpha,m)$, then
$\mathcal{O}^{\prime}\models(\alpha,m)$.

  * •

If $\mathcal{O}^{\prime}\models(\alpha,m)$ and every concept name occurring in
$\alpha$ occurs in $\mathcal{O}$, then $\mathcal{O}\models(\alpha,m)$.

######  Corollary 4.4.

If $\mathcal{O}$ and $\mathcal{O}^{\prime}$ are as in Theorem 4.3, then for
every ${\cal E\\!LHI}_{\bot}$ axiom $\alpha$ over the signature of
$\mathcal{O}$,
$\mathcal{P}(\alpha,\mathcal{O})=\mathcal{P}(\alpha,\mathcal{O}^{\prime})$.

Before describing the reasoning algorithm in detail, we present an important
property of axiom entailment; namely, that all entailment problems can be
polynomially reduced to each other. This allows us to focus on entailment of
annotated assertions.

######  Theorem 4.5.

Let $\mathcal{O}$ be a $\sf{Why}[{\sf X}]$-annotated ${\cal E\\!LHI}_{\bot}$
ontology in normal form, $\alpha$ be a GCI or a RI, and $m$ be a monomial over
${\sf X}$. One can construct in polynomial time a $\sf{Why}[{\sf
X}^{\prime}]$-annotated ${\cal E\\!LHI}_{\bot}$ ontology
$\mathcal{O}^{\prime}$, an assertion $\beta$ and a monomial $n$ over ${\sf
X}^{\prime}$ such that $\mathcal{O}\models(\alpha,m)$ iff
$\mathcal{O}^{\prime}\models(\beta,n)$. Conversely, if $\alpha$ is a concept
(resp. role) assertion and $m$ a monomial over ${\sf X}$, one can construct in
polynomial time a $\sf{Why}[{\sf X}^{\prime}]$-annotated ${\cal
E\\!LHI}_{\bot}$ ontology $\mathcal{O}^{\prime}$, two concept (resp. role)
inclusions $\beta$, $\gamma$ and a monomial $n$ over ${\sf X}^{\prime}$ such
that $\mathcal{O}\models(\alpha,m)$ iff $\mathcal{O}^{\prime}\models(\beta,n)$
or $\mathcal{O}^{\prime}\models(\gamma,n)$.

###### Proof sketch.

First note that when $\mathcal{O}$ is inconsistent, $\mathcal{O}$ trivially
entails every annotated axiom. We thus focus on the case where $\mathcal{O}$
is satisfiable.

We reduce entailment of an annotated ${\cal E\\!LHI}_{\bot}$ GCI
$(C\sqsubseteq D,m_{0})$ to annotated assertion entailment as follows: 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)$.

We show that $\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})$.
For role inclusions, we show that $\mathcal{O}{\models}(P_{1}\sqsubseteq
P_{2},m)$ iff
$\mathcal{O}\cup\\{(P_{1}(a_{0},b_{0}),1)\\}{\models}(P_{2}(a_{0},b_{0}),m)$
where $a_{0},b_{0}$ are fresh individual names.

We reduce entailment of an annotated concept assertion $(B(a_{0}),m_{0})$ to
annotated GCI entailment as follows. For all $a,b\in\mathsf{ind}(\mathcal{O})$
and $R\in{\sf N_{R}}$, assume that the concept or role names $C_{a},R_{ab}$ do
not occur in $\mathcal{O}$ and let

$\displaystyle\mathcal{T}_{C_{a}}=$ $\displaystyle\\{(C_{a}\sqsubseteq
A,v)\mid(A(a),v)\in\mathcal{O}\\}\ \cup$ $\displaystyle\\{(R_{ab}\sqsubseteq
R,v),(C_{a}\equiv\exists R_{ab},1),(C_{b}\equiv\exists
R_{ab}^{-},1)\mid(R(a,b),v)\in\mathcal{O}\\}$ $\displaystyle\mathcal{T}=$
$\displaystyle\bigcup_{a\in\mathsf{ind}(\mathcal{O})}\mathcal{T}_{C_{a}}\cup(\mathcal{O}\setminus\\{(\alpha,v)\mid\alpha\text{
is an assertion}\\}).$

We show that $\mathcal{O}\models(B(a_{0}),m_{0})$ iff
$\mathcal{T}\models(C_{a_{0}}\sqsubseteq B,m_{0})$ or
$\mathcal{T}\models(\top\sqsubseteq B,m_{0})$.

Finally, for role assertions, we show that
$\mathcal{O}\models(R(a_{0},b_{0}),m_{0})$ iff
$\mathcal{T}_{S_{a_{0},b_{0}}}\models(S\sqsubseteq R,m_{0})$ where $S$ is a
fresh role name and

$\displaystyle\mathcal{T}_{S_{a_{0},b_{0}}}=$ $\displaystyle\\{(S\sqsubseteq
R^{\prime},v)\mid(R^{\prime}(a_{0},b_{0}),v)\in\mathcal{O}\\}\cup{}$
$\displaystyle\\{(S\sqsubseteq
R^{\prime-},v)\mid(R^{\prime}(b_{0},a_{0}),v)\in\mathcal{O}\\}\cup{}$
$\displaystyle\\{(P_{1}\sqsubseteq P_{2},v)\mid(P_{1}\sqsubseteq
P_{2},v)\in\mathcal{O}\\}.\qed$

| if | then $\mathcal{S}\leftarrow\mathcal{S}\cup\\{\Phi\\}$
---|---|---
$\mathsf{CR}^{T}_{0}$ | $(A\sqsubseteq\exists P,m_{0}),(P\sqsubseteq P_{1},m_{1}),(P\sqsubseteq P_{2},m_{2}),(P_{1}\sqcap P_{2}\sqsubseteq\bot,m_{3})\in\mathcal{S}$ | $\Phi=(A\sqsubseteq\bot,{m_{0}\times m_{1}\times m_{2}\times m_{3}})$
$\mathsf{CR}^{T}_{1}$ | $(P_{1}\sqsubseteq P_{2},m_{1}),(P_{2}\sqsubseteq P_{3},m_{2})\in\mathcal{S}$ | $\Phi=(P_{1}\sqsubseteq P_{3},{m_{1}\times m_{2}})$
$\mathsf{CR}^{T}_{2}$ | $(M\sqsubseteq A,m_{1}),(A\sqcap N\sqsubseteq C,m_{2})\in\mathcal{S}$ | $\Phi=(M\sqcap N\sqsubseteq C,{m_{1}\times m_{2}})$
$\mathsf{CR}^{T}_{3}$ |  $(A\sqsubseteq\exists Q,m_{0})$, $(Q\sqsubseteq P,m)$, |
|  $(Q\sqsubseteq P_{i},m_{i}),(\exists\mathsf{inv}(P_{i}).A_{i}\sqsubseteq B_{i},n_{i})$, $1\leq i\leq k$, $k\geq 0$, |
|  $(\top\sqsubseteq B^{\prime}_{i},o_{i})$, $1\leq i\leq k^{\prime}$, $k^{\prime}\geq 0$, |
| $(B_{1}\sqcap\dots\sqcap B_{k}\sqcap B^{\prime}_{1}\sqcap\dots\sqcap B^{\prime}_{k^{\prime}}\sqsubseteq C,n),$ | $\Phi=(A\sqcap A_{1}\sqcap\dots\sqcap A_{k}\sqsubseteq D,$
| $(\exists P.C\sqsubseteq D,o)\in\mathcal{S}$ | $m\times n\times o\times m_{0}\times\Pi_{i=1}^{k}(m_{i}\times n_{i})\times\Pi_{i=1}^{k^{\prime}}o_{i})$
$\mathsf{CR}^{A}_{1}$ | $(A_{i}(a),m_{i}),1\leq i\leq k,(A_{1}\sqcap\dots\sqcap A_{k}\sqsubseteq B,m)\in\mathcal{S}$ | $\Phi=(B(a),{m_{1}\times\dots\times m_{k}\times m})$
$\mathsf{CR}^{A}_{2}$ | $(R(a,b),m_{1}),(A(b),m_{2}),(\exists R.A\sqsubseteq B,m_{3})\in\mathcal{S}$ | $\Phi=(B(a),{m_{1}\times m_{2}\times m_{3}})$
$\mathsf{CR}^{A}_{3}$ | $(R(b,a),m_{1}),(A(b),m_{2}),(\exists R^{-}.A\sqsubseteq B,m_{3})\in\mathcal{S}$ | $\Phi=(B(a),{m_{1}\times m_{2}\times m_{3}})$
$\mathsf{CR}^{A}_{4}$ | $(R(a,b),m_{1}),(R\sqsubseteq S,m_{2})\in\mathcal{S}$ | $\Phi=(S(a,b),{m_{1}\times m_{2}})$
$\mathsf{CR}^{A}_{5}$ | $(R(a,b),m_{1}),(R\sqsubseteq S^{-},m_{2})\in\mathcal{S}$ | $\Phi=(S(b,a),{m_{1}\times m_{2}})$
$\mathsf{CR}^{A}_{6}$ | $(R(a,b),m_{1}),(S(a,b),m_{2}),(R\sqcap S\sqsubseteq\bot,m_{3})\in\mathcal{S}$ | $\Phi=(\bot(a),{m_{1}\times m_{2}\times m_{3}})$
$\mathsf{CR}^{A}_{7}$ | $(R(a,b),m_{1}),(S(b,a),m_{2}),(R\sqcap S^{-}\sqsubseteq\bot,m_{3})\in\mathcal{S}$ | $\Phi=(\bot(a),{m_{1}\times m_{2}\times m_{3}})$

Table 2: Completion rules. $A_{(i)},B_{(i)},C,D\in{\sf
N_{C}}\cup\\{\top,\bot\\}$, $R,S\in{\sf N_{R}}$, $P_{(i)},Q:=R\mid R^{-}$,
$M,N$ are (possibly empty) conjunctions over ${\sf N_{C}}\cup\\{\top\\}$, and
$m_{(i)},n_{(i)},o_{(i)}\in\mathsf{mon}({\sf X})$ (recall that since $\times$
is idempotent, monomials do not contain repeated variables). Conjunctions are
treated as sets (no repetition and the order does not matter; we assume that
conjunctions are written in lexicographic order). Empty conjunctions are
written $\top$ and non-empty conjunctions are written without $\top$ (in
particular in $\mathsf{CR}^{T}_{3}$, if some but not all $A_{i}$ are equal to
$\top$, they do not explicitely occur in the conjunction $A\sqcap
A_{1}\sqcap\dots\sqcap A_{k}$).

####  4.1.2 Completion Algorithm

We adapt the ${\cal E\\!LHI}_{\bot}$ completion rules (?, Section 4.3) to
handle annotated ${\cal E\\!LHI}_{\bot}$ ontologies in normal form. We cannot
use directly the rules presented by ? because they require qualified role
restrictions on the right side of the inclusion and may have superfluous
premises that will induce wrong provenance information as illustrated in the
example below.

######  Example 4.6.

Consider the following annotated ontology:

$\displaystyle\mathcal{O}=\\{(\top\sqsubseteq A_{1},v_{1}),(\top\sqsubseteq
A_{2},v_{2}),(B\sqsubseteq\exists R,v),(\exists R.A_{1}\sqsubseteq
C,u),(B(a),w)\\}$

If we apply the completion rules given by ? and naively propagate the premises
monomials to the consequences, we obtain the following axioms:
$(B\sqsubseteq\exists R.A_{1},vv_{1})$ (by rule T6), $(B\sqsubseteq\exists
R.(A_{1}\sqcap A_{2}),vv_{1}v_{2})$ (by rule T6), $(B\sqsubseteq
C,vv_{1}v_{2}u)$ (by rule T7) and $(C(a),vv_{1}v_{2}uw)$ (by rule A1).
However, $\mathcal{O}\not\models(C(a),vv_{1}v_{2}uw)$. This comes from the
fact that rule T7 presented by ? can be applied on $B\sqsubseteq\exists
R.(A_{1}\sqcap A_{2})$ and $\exists R.A_{1}\sqsubseteq C$ to get $B\sqsubseteq
C$ while $B\sqsubseteq\exists R.(A_{1}\sqcap A_{2})$ is a too precise premise
in our context. ∎

Hence we designed rules for completing $\sf{Why}[{\sf X}]$-annotated ${\cal
E\\!LHI}_{\bot}$ ontologies. The completion algorithm starts with the original
ontology completed with some trivially entailed axioms expressed in an
extension of ${\cal E\\!LHI}_{\bot}$ (featuring, e.g. assertions of the form
$(\top(a),1)$):

$\displaystyle\mathcal{S}:=\mathcal{O}$ $\displaystyle\cup\\{(\top(a),1)\mid
a\in\mathsf{ind}(\mathcal{O})\\}$ $\displaystyle\cup\\{(A\sqsubseteq A,1)\mid
A\in({\sf N_{C}}\cap\mathsf{sig}(\mathcal{O}))\cup\\{\top,\bot\\}\\}$
$\displaystyle\cup\\{(R\sqsubseteq R,1),(R^{-}\sqsubseteq R^{-},1),(\exists
R.\bot\sqsubseteq\bot,1),(\exists R^{-}.\bot\sqsubseteq\bot,1)\mid R\in{\sf
N_{R}}\cap\mathsf{sig}(\mathcal{O})\\}$
$\displaystyle\cup\\{(\mathsf{inv}(P_{1})\sqsubseteq\mathsf{inv}(P_{2}),m)\mid(P_{1}\sqsubseteq
P_{2},m)\in\mathcal{O}\\}$
$\displaystyle\cup\\{(\mathsf{inv}(P_{1})\sqcap\mathsf{inv}(P_{2})\sqsubseteq\bot,m)\mid(P_{1}\sqcap
P_{2}\sqsubseteq\bot,m)\in\mathcal{O}\\}.$

Contrary to the saturation procedure described by ?, we do not add the axiom
$A\sqsubseteq\top$: since
$\top^{\mathcal{I}}=\Delta^{\mathcal{I}}\times\\{1\\}$, $(A\sqsubseteq\top,1)$
does not hold in general.

After this initialization step, the completion algorithm extends $\mathcal{S}$
with axioms through an iterative application of the rules from Table 2 until
$\mathcal{S}$ becomes _saturated_ ; i.e., no more rules are applicable. To
ensure termination, a rule is applicable only if it modifies $\mathcal{S}$.
The axioms added by the completion rules respect the syntactic restriction of
${\cal E\\!LHI}_{\bot}$ but may not be in normal form. In particular,
conjunctions of arbitrary size (bounded by the number of concept names that
occur in $\mathcal{O}$) can be introduced in the left-hand side of GCIs by
$\mathsf{CR}^{T}_{2}$ and $\mathsf{CR}^{T}_{3}$. To avoid introducing
qualified role restrictions in the right-hand side, $\mathsf{CR}^{T}_{3}$
performs the equivalent of several classical “completion steps” at once. For
example, on the annotated ontology of Example 4.6, $\mathsf{CR}^{T}_{3}$
produces directly $(B\sqsubseteq C,vv_{1}u)$.

The algorithm may add axioms annotated with monomials, which are not foreseen
in the definition of $\sf{Why}[{\sf X}]$-annotated ontologies, but
$\times$-idempotency ensures that all monomials have at most $|\mathcal{O}|$
factors. We show that the completion algorithm is sound and complete for
deciding assertion entailment and runs in exponential time.

######  Theorem 4.7.

Let $\mathsf{saturate}(\mathcal{O})$ be the result of saturating
$\mathcal{O}$, $m\in\mathsf{mon}({\sf X})$, and $\alpha$ be an _assertion_.

  1. 1.

If $(\alpha,m)\in\mathsf{saturate}(\mathcal{O})$ then
$\mathcal{O}\models(\alpha,m)$.

  2. 2.

If $\mathcal{O}$ is satisfiable and $\mathcal{O}\models(\alpha,m)$, then
$(\alpha,m)\in\mathsf{saturate}(\mathcal{O})$.

  3. 3.

If $\mathcal{O}$ is unsatisfiable,
$(\bot(a),n)\in\mathsf{saturate}(\mathcal{O})$ for some
$a\in\mathsf{ind}(\mathcal{O})$ and $n\in\mathsf{mon}({\sf X})$.

  4. 4.

$\mathsf{saturate}(\mathcal{O})$ is computable in exponential time w.r.t. the
size of $\mathcal{O}$.

Due to Theorems 4.7 and 4.5, we obtain the following corollaries.

######  Corollary 4.8.

If $\mathcal{O}$ is a $\sf{Why}[{\sf X}]$-annotated ${\cal E\\!LHI}_{\bot}$
ontology, for every axiom $\alpha$ and monomial $m\in\mathsf{mon}({\sf X})$,
$\mathcal{O}\models(\alpha,m)$ is decidable in exponential time in
$|\mathcal{O}|$.

######  Corollary 4.9.

If $\mathcal{O}$ is a $\sf{Why}[{\sf X}]$-annotated ${\cal E\\!LHI}_{\bot}$
ontology, for every axiom $\alpha$, the provenance
$\mathcal{P}(\alpha,\mathcal{O})=\sum_{\mathcal{O}\models(\alpha,m)}m$ can be
computed in exponential time w.r.t. $|\mathcal{O}|$.

Since subsumption in $\mathcal{ELI}$ is ExpTime-hard (?), we obtain a matching
lower bound for the axiom entailment problem and cannot hope for computing the
why-provenance of axioms in ${\cal E\\!LHI}_{\bot}$ more efficiently. However,
there is an additional source of complexity when considering provenance, as
illustrated by the following example that shows an exponential blow-up already
for a simple ontology for which axiom entailment could be done in polynomial
time if the provenance annotations were ignored.

######  Example 4.10.

Consider $\mathcal{O}=\\{(A\sqsubseteq A_{i},v_{i}),(A_{i}\sqsubseteq
B,u_{i})\mid 0\leq i\leq n\\}\cup\\{(B\sqsubseteq A,u)\\}$. For every
$S\subseteq\\{1,\dots,n\\}$, $(B\sqsubseteq A,u\times\Pi_{i\in S}u_{i}\times
v_{i})\in\mathsf{saturate}(\mathcal{O})$. ∎

####  4.1.3 The Case of Lightweight DLs

We show that in the fragment $\mathcal{ELHI_{\bot}^{\mathit{restr}}}$ (cf.
Definition 2.1) which includes in particular ${\cal E\\!LH}^{r}$ and DL-LiteR,
the exponential complexity of deciding annotated axiom entailment comes only
from the size of the monomial.

######  Theorem 4.11.

If $\mathcal{O}$ belongs to $\mathcal{ELHI_{\bot}^{\mathit{restr}}}$, then for
every axiom $\alpha$ and monomial $m$, $\mathcal{O}\models(\alpha,m)$ is
decidable in polynomial time in $|\mathcal{O}|$ and in exponential time in
$|m|$.

We show this theorem by slightly modifying the completion algorithm. First, we
restrict the rules from Table 2 that may introduce exponentially many axioms,
and add two additional rules $\mathsf{CR}^{T}_{4}$ and $\mathsf{CR}^{T}_{5}$
as follows:

  * •

$\mathsf{CR}^{T}_{2}$ is restricted by fixing $|M|\leq 2$ and $N$ is empty.
This amounts to replacing $\mathsf{CR}^{T}_{2}$ with the more specific rule:

“if $(B_{1}\sqcap B_{2}\sqsubseteq A,m_{1}),(A\sqsubseteq
C,m_{2})\in\mathcal{S}$ then substitute $\mathcal{S}$ with
$\mathcal{S}\cup\\{\Phi\\}$ where $\Phi=(B_{1}\sqcap B_{2}\sqsubseteq
C,{m_{1}\times m_{2}})$.”

  * •

$\mathsf{CR}^{T}_{3}$ is restricted by fixing $k+k^{\prime}\leq 2$ and
$A_{i}=\top$ for every $1\leq i\leq k$. This amounts to replacing
$\mathsf{CR}^{T}_{3}$ by the more specific rule:

“given $k,k^{\prime}\geq 0$ such that $k+k^{\prime}\leq 2$, if it holds that
$(A\sqsubseteq\exists Q,m_{0})$, $(Q\sqsubseteq P,m)$, $(Q\sqsubseteq
P_{i},m_{i})$, $(\exists\mathsf{inv}(P_{i}).\top\sqsubseteq B_{i},n_{i})$ for
$1\leq i\leq k$, $(\top\sqsubseteq B^{\prime}_{i},o_{i})$ for $1\leq i\leq
k^{\prime}$, $(B_{1}\sqcap\dots\sqcap B_{k}\sqcap
B^{\prime}_{1}\sqcap\dots\sqcap B^{\prime}_{k^{\prime}}\sqsubseteq C,n)$ (note
that the conjunction contains at most two concept names since
$k+k^{\prime}\leq 2$), and $(\exists P.C\sqsubseteq D,o)\in\mathcal{S}$, then
$\mathcal{S}\leftarrow\mathcal{S}\cup\\{\Phi\\}$ where $\Phi=(A\sqsubseteq
D,m\times n\times o\times m_{0}\times\Pi_{i=1}^{k}(m_{i}\times
n_{i})\times\Pi_{i=1}^{k^{\prime}}o_{i})$.”

  * •

$\mathsf{CR}^{T}_{4}$ is defined by:

“given $k,k^{\prime}\geq 0$ such that $k+k^{\prime}\leq 2$, if $(P\sqsubseteq
P_{i},m_{i}),(\exists P_{i}.\top\sqsubseteq B_{i},n_{i})$ for $1\leq i\leq k$,
$(\top\sqsubseteq B^{\prime}_{i},o_{i})$ for $1\leq i\leq k^{\prime}$, and
$(B_{1}\sqcap\dots\sqcap B_{k}\sqcap B^{\prime}_{1}\sqcap\dots\sqcap
B^{\prime}_{k^{\prime}}\sqsubseteq C,n)$ are in $\mathcal{S}$, then
$\mathcal{S}\leftarrow\mathcal{S}\cup\\{\Phi\\}$ where $\Phi=(\exists
P.\top\sqsubseteq C,n\times\Pi_{i=1}^{k}(m_{i}\times
n_{i})\times\Pi_{i=1}^{k^{\prime}}o_{i})$.”

  * •

$\mathsf{CR}^{T}_{5}$ is defined by:

“if $(\top\sqsubseteq A_{1},m_{1})$, $(\top\sqsubseteq A_{2},m_{2})$ and
$(A_{1}\sqcap A_{2}\sqsubseteq B,n)$ are in $\mathcal{S}$, then
$\mathcal{S}\leftarrow\mathcal{S}\cup\\{\Phi\\}$ where $\Phi=(\top\sqsubseteq
B,m_{1}\times m_{2}\times n)$.”

Second, we let $\mathsf{saturate}^{k}(\mathcal{O})$ be the $k$-saturation of
$\mathcal{O}$, i.e. the annotated ontology obtained from $\mathcal{O}$ through
the modified completion rules restricted to monomials of size at most $k$
(i.e. that have at most $k$ variables).

We show (1) that $\mathsf{saturate}^{k}(\mathcal{O})$ can be computed in
polynomial time w.r.t. the size of $\mathcal{O}$ and exponential time w.r.t.
$k$, (2) that when $\mathcal{O}$ is satisfiable,
$\mathsf{saturate}^{k}(\mathcal{O})$ suffices for deciding entailment of
annotated assertions $(\alpha,m)$ where $m$ is a monomial of size at most $k$,
and (3) that the algorithm can be modified by ignoring the monomials in the
annotated axioms to check in polynomial time whether $\mathcal{O}$ is
satisfiable (which shows the complexity of satisfiability in
$\mathcal{ELHI_{\bot}^{\mathit{restr}}}$ given in Theorem 2.2).

It follows that we can first check that $\mathcal{O}$ is satisfiable in
polynomial time, then compute $\mathsf{saturate}^{|m|}(\mathcal{O})$ in
polynomial time w.r.t. the size of $\mathcal{O}$ and exponential time w.r.t.
$|m|$ to decide whether $\mathcal{O}\models(\alpha,m)$.

###  4.2 Conjunctive Queries over ${\cal E\\!LHI}_{\bot}$ Ontologies

We have seen that ${\cal E\\!LHI}_{\bot}$ is expressive enough to reduce
entailment of rooted tree-shaped BCQs to assertion entailment (cf. Theorem
3.10). However, this does not apply to general BCQs that may, for example,
contain cycles. To deal with such queries, we adapt the method for conjunctive
query answering in ${\cal E\\!LHI}_{\bot}$ described by ? (?, Section 5.2). In
a nutshell, the idea is to rewrite some parts of the query w.r.t. the
saturated ontology into a query that can be matched in the assertions of the
saturated ontology.

In this section, we assume (w.l.o.g. by Theorem 4.3) that $\mathcal{O}$ is a
$\sf{Why}[{\sf X}]$-annotated ${\cal E\\!LHI}_{\bot}$ ontology in _normal
form_ and we let $\mathsf{saturate}(\mathcal{O})$ be the result of saturating
$\mathcal{O}$.

######  Definition 4.12 (Adapted from Definition 8 of ? (?)).

For a CQ $q$, a monomial $m$ and a $\sf{Why}[{\sf X}]$-annotated ${\cal
E\\!LHI}_{\bot}$ ontology $\mathcal{O}$ in normal form, we write
$(q,m)\rightarrow_{\mathcal{O}}(q^{\prime},m^{\prime})$ if
$(q^{\prime},m^{\prime})$ can be obtained from $(q,m)$ by applying the
following steps.

  * (S1)

Select in $q$ an arbitrary existentially quantified variable $x_{0}$ such that
there are no atoms of the form $R(x_{0},x_{0})$ in $q$.

  * (S2)

Replace each role atom of the form $R(x_{0},y)$ in $q$, where $y$ and $R$ are
arbitrary, by the atom $\mathsf{inv}(R)(y,x_{0})$.

  * (S3)

Let $V_{p}=\\{y\mid Q(y,x_{0})\in q\text{ for some }Q\\}$ and select some
$(A\sqsubseteq\exists P,v)\in\mathcal{O}$ (recall that $A\in{\sf N_{C}}$ since
$\mathcal{O}$ is in normal form) such that:

    * (a)

for every $Q(y,x_{0})\in q$, there is some $(P\sqsubseteq Q,m_{P\sqsubseteq
Q})\in\mathsf{saturate}(\mathcal{O})$;

    * (b)

for every $C(x_{0})\in q$, there exist $p,p^{\prime}\geq 0$ such that
$(B_{1}{\sqcap}\dots\sqcap B_{p}\sqcap B^{\prime}_{1}{\sqcap}\dots\sqcap
B^{\prime}_{p^{\prime}}\sqsubseteq C,n_{C})\in\mathsf{saturate}(\mathcal{O})$
and

      * *

for every $1\leq i\leq p$, there exist
$(\exists\mathsf{inv}(P_{i}).A_{i}\sqsubseteq B_{i},v_{i})\in\mathcal{O}$ and
$(P\sqsubseteq P_{i},m_{i})\in\mathsf{saturate}(\mathcal{O})$ and

      * *

for every $1\leq i\leq p^{\prime}$, there exists $(\top\sqsubseteq
B^{\prime}_{i},o_{i})\in\mathsf{saturate}(\mathcal{O})$.

Let $At(q,x_{0},A\sqsubseteq\exists P)=\\{A\\}$ and
$mon(q,x_{0},A\sqsubseteq\exists P)=v$.

    * (a)

For every $Q(y,x_{0})\in q$, arbitrarily select one $(P\sqsubseteq
Q,m_{P\sqsubseteq Q})$ in $\mathsf{saturate}(\mathcal{O})$ and update
$mon(q,x_{0},A\sqsubseteq\exists P)\leftarrow mon(q,x_{0},A\sqsubseteq\exists
P)\times m_{P\sqsubseteq Q}$.

    * (b)

For every $C(x_{0})\in q$, arbitrarily select some $(B_{1}\sqcap\dots\sqcap
B_{p}\sqcap B^{\prime}_{1}\sqcap\dots\sqcap B^{\prime}_{p^{\prime}}\sqsubseteq
C,n_{C})\in\mathsf{saturate}(\mathcal{O})$, for every $1\leq i\leq p$ select
arbitrarily a pair $(\exists\mathsf{inv}(P_{i}).A_{i}\sqsubseteq
B_{i},v_{i})\in\mathcal{O}$ and $(P\sqsubseteq
P_{i},m_{i})\in\mathsf{saturate}(\mathcal{O})$, and for every $1\leq i\leq
p^{\prime}$ select arbitrarily some $(\top\sqsubseteq
B^{\prime}_{i},o_{i})\in\mathsf{saturate}(\mathcal{O})$. Update
$At(q,x_{0},A\sqsubseteq\exists P)\leftarrow At(q,x_{0},A\sqsubseteq\exists
P)\cup\\{A_{i}\mid 1\leq i\leq p\\}$ and $mon(q,x_{0},A\sqsubseteq\exists
P)\leftarrow mon(q,x_{0},A\sqsubseteq\exists P)\times n_{C}\times m_{C}$ where
$m_{C}=\prod_{i=1}^{p}(v_{i}\times m_{i})\times\prod_{i=1}^{p^{\prime}}o_{i}$.

  * (S4)

Drop from $q$ every atom that contains $x_{0}$.

  * (S5)

Select a variable $y_{0}\in V_{p}$ and replace every occurrence of
$y^{\prime}\in V_{p}$ in $q$ by $y_{0}$.

  * (S6)

Add the atoms $\\{D(y_{0})\mid D\in At(q,x_{0},A\sqsubseteq\exists P)\\}$ to
$q$ and multiply $m$ by $mon(q,x_{0},A\sqsubseteq\exists P)$.

We write $(q,1)\rightarrow_{\mathcal{O}}^{*}(q^{*},m^{*})$ if
$(q,1)=(q_{0},m_{0})$ and $(q^{*},m^{*})=(q_{k},m_{k})$ for some finite
rewriting sequence
$(q_{0},m_{0})\rightarrow_{\mathcal{O}}(q_{1},m_{1})\rightarrow_{\mathcal{O}}\dots\rightarrow_{\mathcal{O}}(q_{k},m_{k})$
for $k\geq 0$, and we say that the set
$\mathsf{Rew}(q,\mathcal{O})=\\{(q^{*},m^{*})\mid(q,1)\rightarrow_{\mathcal{O}}^{*}(q^{*},m^{*})\\}$
is the _annotated rewriting of $q$ w.r.t. $\mathsf{saturate}(\mathcal{O})$_.

Note that there may be exponentially many pairs of the form
$(q^{*},m_{1}),(q^{*},m_{2}),\dots$ in $\mathsf{Rew}(q,\mathcal{O})$ since the
same query $q^{*}$ can be obtained by choosing different annotated inclusions
in the rewriting steps and an axiom can be annotated with exponentially many
monomials in $\mathsf{saturate}(\mathcal{O})$ (cf. Example 4.10).

######  Theorem 4.13.

Let $\mathcal{O}$ be a satisfiable $\sf{Why}[{\sf X}]$-annotated ${\cal
E\\!LHI}_{\bot}$ ontology in normal form, $q(\vec{x})$ be a CQ and $\vec{a}$
be a tuple of individuals from $\mathcal{O}$ of the same arity as $\vec{x}$.
We denote by $\mathcal{O}^{\prime}$ the non-annotated version of
$\mathcal{O}$, by $\mathcal{D}$ the set of annotated assertions in
$\mathsf{saturate}(\mathcal{O})$ and by $\mathcal{D}^{\prime}$ the
corresponding set of (non-annotated) assertions. Then

  1. 1.

$\mathcal{O}^{\prime}\models q(\vec{a})$ iff there is some
$(q^{*},m^{*})\in\mathsf{Rew}(q(\vec{a}),\mathcal{O})$ such that there is a
match for $q^{*}(\vec{a})$ in $\mathcal{D}^{\prime}$.

  2. 2.

For every $m\in\mathsf{mon}({\sf X})$, $\mathcal{O}\models(q(\vec{a}),m)$ iff
there is some $(q^{*},m^{*})\in\mathsf{Rew}(q(\vec{a}),\mathcal{O})$ such that
$\mathcal{D}\models(q^{*}(\vec{a}),o)$ for some $o\in\mathsf{mon}({\sf X})$
such that $m=m^{*}\times o$.

  3. 3.

$\mathcal{P}(q(\vec{a}),\mathcal{O})=\sum_{(q^{*},m^{*})\in\mathsf{Rew}(q,\mathcal{O})}m^{*}\times\mathcal{P}(q^{*}(\vec{a}),\mathcal{D})$.

  4. 4.

$\mathsf{Rew}(q,\mathcal{O})$ is computable in exponential time in
$|\mathcal{O}|$ and $|q|$.

We show that for every $(q^{*},m^{*})\in\mathsf{Rew}(q,\mathcal{O})$,
$(q^{*},m^{*})$ is of polynomial size, which yields the following corollaries
of Theorems 4.13 and 4.7.

######  Corollary 4.14.

If $\mathcal{O}$ is a satisfiable $\sf{Why}[{\sf X}]$-annotated ${\cal
E\\!LHI}_{\bot}$ ontology, for every BCQ $q$ and $m\in\mathsf{mon}({\sf X})$,
$\mathcal{O}\models(q,m)$ is decidable in exponential time w.r.t.
$|\mathcal{O}|$ and $|q|$.

######  Corollary 4.15.

If $\mathcal{O}$ is a satisfiable $\sf{Why}[{\sf X}]$-annotated ${\cal
E\\!LHI}_{\bot}$ ontology, for every BCQ $q$, the provenance
$\mathcal{P}(q,\mathcal{O})$ can be computed in exponential time w.r.t.
$|\mathcal{O}|$ and $|q|$.

Since BCQ entailment is already ExpTime-complete for ${\cal E\\!LHI}_{\bot}$
without annotations (?), we cannot hope for a better complexity upper bound.
However, if we restrict ourselves to ontologies expressed in
$\mathcal{ELHI_{\bot}^{\mathit{restr}}}$, we can obtain a result similar to
Theorem 4.11 for annotated BCQ entailment.

######  Theorem 4.16.

If $\mathcal{O}$ is an $\mathcal{ELHI_{\bot}^{\mathit{restr}}}$ ontology, then
for every BCQ $q$ and monomial $m$, $\mathcal{O}\models(q,m)$ is decidable in
NP w.r.t. $|\mathcal{O}|$ and $|q|$ (with $|m|$ fixed), and in exponential
time in $|m|$.

A matching NP lower bound comes from the combined complexity of standard BCQ
entailment over databases. Note that for the specific cases of DL-LiteR and
${\cal E\\!LH}^{r}$, ? (?) and ? (?) proposed algorithms for annotated BCQ
entailment with some $\sf{Why}[{\sf X}]$-provenance annotations, respectively
by adapting classical query rewriting algorithm for DL-LiteR (?) and the
combined approach based on the computation of a compact canonical model for
${\cal E\\!LH}^{r}$ (?).

##  5 Computing Provenance in More Constrained Semirings

In this section, we study the cases of $\oplus$\- and $\otimes$-idempotent
semirings that are also absorptive (such that $a\otimes b\oplus a=a$) or such
that for every $a,b\neq\mathbb{0}$, $a\oplus b=a\otimes b$ (denoted by
$\oplus\approx\otimes$). The universal provenance semiring for semirings that
are absorptive and $\otimes$-idempotent (recall that every absorptive semiring