In ontology-mediated query answering, access to incomplete data sources is mediated by a conceptual layer constituted by an ontology. To correctly compute answers to queries, it is necessary to perform complex reasoning over the constraints expressed by the ontology. In the literature, there exists a multitude of techniques incorporating the ontological knowledge into queries. However, few of these approaches were designed for comprehensibility of the query answers. In this article, we try to bridge these two qualities by adapting a proof framework originally applied to axiom entailment for conjunctive query answering. We investigate the data and combined complexity of determining the existence of a proof below a given quality threshold, which can be measured in diferent ways. By distinguishing various parameters such as the shape of a query, we obtain an overview of the complexity of this problem for the lightweight ontology languages DL-Lite,and also have a brief look at temporal query answering.
Explaining description logic (DL) reasoning has a long tradition, starting with the first works on
proofs for standard DL entailments [
Here, we also investigate proofs for CQ answers, inspired by [18, 19, 20], but additionally
consider the problem of generating good proofs according to some quality measures and provide
a range of complexity results focussing on DL-Lite.In addition to classical OMQA, we also have
a brief look at explaining inferences over temporal data using a query language incorporating
metric temporal operators. Our results are based on a framework developed for proofs of
standard DL reasoning [
In this paper, we consider two diferent kinds of derivers for generating proofs for CQ answers. These loosely correspond to the approaches in [18, 19, 20], but are generalized to apply to a larger class of DLs. Specifically, our structures rely on a translation of DLs to existential rules [22], and thus apply to any DL that can be expressed in this formalism. One deriver, denoted by Dcq and inspired by [19, 20], focuses on the derivation of CQs, which can be derived from other CQs and ontology axioms. Inferences in Dcq are logically sound, but can be harder to understand. The reason is the local scope of existential quantification in a CQ, which forces atoms connected by the same variables to be carried along inferences they are not relevant for. This problem is circumvented with the deriver Dsk, which relies on a Skolemized version of the TBox. This allows one to focus on inferences of single atoms that are only later aggregated into the final CQ, leading to simpler sentences within the proof. Focusing on the particular cases of DL-Lite and ℰℒ, we consider the complexity of the decision problems of finding proofs of (tree) size below a given threshold in these derivation structures. We find that for DL-Lite and any DL in which CQ answering is UCQ-rewritable, all of these problems (regardless of derivation structure and quality measure) are in AC0 in data complexity. In combined complexity, these problems are NP-complete in general, but polynomial when considering only acyclic queries and tree size. We also obtain similar results for the case of Dsk w.r.t. ℰℒ ontologies and tree size, but for size the situation is not clear yet because we suspect that for ℰℒ proofs may actually get exponentially large. To explain answers to temporal queries, we extend our derivers with new inference schemes to deal with metric temporal operators, allowing us to lift some of our results also to this setting. The full details can be found in a technical report [23], but we describe the main ideas here.
Proofs In our setting, a logic ℒ = (ℒ, |=ℒ) consists of a set ℒ of ℒ-sentences and a consequence relation |=ℒ ⊆ (ℒ) × ℒ between ℒ-theories (subsets of ℒ-sentences) and single ℒ-sentences; we usually write only |= instead of |=ℒ. We assume that the size | | of an ℒsentence is defined in some way, e.g. by the number of symbols in . We require that ℒ is monotonic, i.e. that |= implies ′ |= for all ′ ⊇ . For example, ℒ could be first-order logic or some DL.
As in [
We call hyperedges (, ) ∈ inferences or inference steps, with being the premises and the conclusion, and may write them like → or →
Definition 2 (Proof). Given a sentence and a theory , a proof of |= is a finite derivation structure = (, , ℓ) over such that • contains exactly one sink ∈ , which is labeled by , • is acyclic, and • every vertex has at most one incoming hyperedge, i.e. there exist no two hyperedges (1, ), (2, ) ∈ with 1 ̸= 2.
A tree proof is a proof that is a tree. A subproof of a hypergraph is a subgraph of that is a proof with leaf() ⊆ leaf().
To compute proofs, we assume that there is some reasoning system or calculus that defines
a derivation structure for a given entailment , and the structure may contain several proofs
for that entailment. Formally, a deriver D for a logic ℒ takes as input an ℒ-theory and an
ℒ-sentence , and returns a (possibly infinite) derivation structure D( , ) over that describes
all inference steps that D could perform in order to derive from . This derivation structure
is not necessarily computed explicitly, but can be accessed through an oracle (which checks,
for example, whether an inference conforms to the underlying calculus). The task of finding a
good proof then corresponds to finding a (finite) proof that can be homomorphically mapped
into this derivation structure and which is minimal according to some measure of proof quality.
We consider two such measures here: the size of a proof = (, , ℓ) is ms() := | |,1 and
the tree size mt() is the size of a tree unraveling of [
DLs and Existential Rules We assume that the reader is familiar with DLs, in particular DL-Lite [24] and ℰℒ [25], where theories = ∪ are called ontologies or knowledge bases and are composed of a TBox and an ABox . Many DL ontologies can be equivalently expressed using the formalism of existential rules [22]. Existential rules are first-order sentences of the form ∀⃗, ⃗. (⃗, ⃗) → ∃⃗. (⃗, ⃗), with the body (⃗, ⃗) and the head (⃗, ⃗) being conjunctions of atoms of the form () or (1, 2), for a concept name , role name and terms , 1 and 2, which are individual names or variables from ⃗, ⃗ and ⃗. We usually omit the universal quantification. Notable DLs that can be equivalently expressed as sets of existential rules are ℰℒ, Horn-ℛℐ and DL-Lite. 1Since every vertex has at most one incoming hyperedge, the size of is at most quadratic in | |. Conjunctive Queries In this paper, we want to construct proofs for ontology-mediated conjunctive query entailments. A conjunctive query (CQ) q(⃗) is an expression of the form ∃⃗. (⃗, ⃗), where (⃗, ⃗) is a conjunction of atoms using answer variables ⃗ and existentially quantified variables ⃗. If ⃗ = (), then q(⃗) is called Boolean. ABox assertions are a special case of Boolean CQs with only one atom and no variables. A tuple ⃗ of individual names from is a certain answer to q(⃗) over ∪ , in symbols ∪ |= q(⃗), if, for any model of ∪ , the sentence q(⃗) is true in this model. Any CQ q(⃗) = ∃⃗. (⃗, ⃗) is associated with the set of atoms in , so we can write e.g. () ∈ q(⃗).
Example 1. For the following DL-Lite ontology and query, we have ∪ {(b)} |= q(b).
= { ⊑ ∃, ∃− ⊑ ∃, ⊑ ∃, ∃ − ⊑ ∃, ⊑ − } q(′′) = ∃, ′, ′′, , ′, , ′. (, ) ∧ (, ) ∧ (′, ) ∧ (′, ′) ∧ (′, ′) ∧ (′′, ′) ∧ (′′, ′′).
In the next section, we explore diferent ways to explain this inference (see Figures 2 and 4).
In the following, let ∪ be a knowledge base in some DL ℒ, q a conjunctive query, and ⃗ a certain answer, i.e. ∪ |= q(⃗), which we want to explain. We can use derivation structures over ℒcq (the extension of ℒ with all Boolean CQs) to explain query answers. For example, the following derivation step involving the ontology from Example 1 is a sound inference: (b) q(b)
However, to define a derivation structure that yields proofs suitable for explanations to users,
inferences that only make small deduction steps are more valuable. For this purpose, we define
derivers that capture which inference steps are admitted. For TBox entailment, in [
Similarly to the approach used in [19, 20], inferences in our first deriver, Dcq, always produce Boolean CQs. This deriver is defined for DLs that can be expressed using existential rules. An inference step is obtained by matching the left-hand side of a rule to part of a CQ and then replacing it by the right-hand side. For example, starting from ∃. (b, ) and (, ) → (, ), we can apply the substitution { ↦→ b, ↦→ } to obtain ∃. (, b). Additionally, we allow to keep any of the replaced atoms from the original CQ, e.g. to produce the conclusion ∃. (b, ) ∧ (, b). A second type of inference allows one to combine two Boolean CQs using conjunction. To duplicate variables, we additionally introduce tautological rules such as (, ) → ∃′. (, ′), ∃⃗. (⃗) (⃗, ⃗) → ∃⃗. (⃗, ⃗) ∃⃗. (⃗)
(MP) (⃗, ⃗) → ∃⃗. (⃗, ⃗) (T) ∃⃗. (⃗)
∃⃗. (⃗) ∃⃗, ⃗′.(⃗) ∧ (⃗′)
(C) ∃⃗. (⃗, ⃗) ∃⃗, ⃗. (⃗, ⃗) (E) which yields ∃, ′. (b, ) ∧ (b, ′) when combined with ∃. (b, ). Finally, we use an inference schema that allows us to replace constants by variables, e.g. to capture that ∃. (b, ) implies ∃, . (, ).
The detailed inference schemas can be found in Figure 1. (MP) is admissible only if there exists a substitution such that ( (⃗, ⃗)) ⊆ (⃗), and then (⃗) is the result of replacing any subset of ( (⃗, ⃗)) in (⃗) by any subset of ( (⃗, ⃗′)), where the variables ⃗ are renamed into new existentially quantified variables ⃗′ to ensure that they are disjoint with ⃗. In (C), we again rename the variables ⃗ to ⃗′ to avoid overlap with ⃗. Since every ABox assertion corresponds to a ground CQ, this inference also allows one to collect ABox assertions into a single CQ. (T) introduces an existential rule that allows us, together with (MP), to create copies of variables in CQs (see Fig. 2). Finally, (E) transforms individual names in some positions into existentially quantified variables.
Definition 3 (CQ Deriver). Dcq( ∪ , q(⃗)) is a derivation structure over ∪ with vertices labeled by the axioms in ∪ and all Boolean CQs over the signature of ∪ , and its hyperedges represent all possible instances of (MP), (C), (T), and (E) over these vertices. An (admissible) proof in Dcq( ∪ , q(⃗)) is a proof of ∪ |= q(⃗) that has a homomorphism into this derivation structure.
It is easy to check that the inferences used by Dcq are sound. Moreover, we can show that they are complete, i.e. that any CQ entailed by ∪ has a proof in Dcq( ∪ , q(⃗)) (see Lemma 5). A proof for Example 1 w.r.t. Dcq is depicted in Figure 2.
To explain a Boolean CQ, using a derivation structure that works on CQs seems natural. However, a downside is that we have to “collect” quantified variables along the proof and label vertices with complex expressions. Since the inference rules apply on sub-expressions, it may be challenging to understand on which part of the CQ an inference is performed—indeed, finding a match for the body o a rule in a CQ is NP-hard. The problem is that we cannot separate inference steps on the same variable without afecting soundness, as the existential quantification only applies locally in the current CQ. To follow our example: ′′ and ′ in Figure 2 are connected to each other and to the constant b, and thus have to be kept together: although ∃′′, ′. (b, ′′) ∧ (′′, ′) implies ∃′′. (b, ′′) and ∃′′, ′.(′′, ′), those two CQs do not imply the original CQ anymore. To overcome these issues, we consider a second type of deriver that relies on Skolemization, and is inspired by the approach from [18].
∃′′, ′ (b, ′′) ∧ (′′, ′) (b)
(MP) ∃′′. (b, ′′) (MP) (MP) ∃ − ⊑ ∃ ∃′′, ′. (′′, b) ∧ (′′, ′) ∧ (b, ′′) (MP) ∃′′, , ′. (′′, b) ∧ (b, ) ∧ (′′, ′) ∧ (b, ′′) ∃′′, ′, , ′. (′′, b) ∧ (b, ) ∧ (′, ) ∧ (′′, ′) ∧ . . . . . . ∃, ′, ′′, ′, , ′. (, b) ∧ (b, ) ∧ (′, ) ∧ (′, ′) ∧ (′, ′) ∧ (′′, ′) ∧ (b, ′′) (E) ∃, ′, ′′, , ′, , ′. (, ) ∧ (, ) ∧ (′, ) ∧ (′, ′) ∧ (′, ′) ∧ (′′, ′) ∧ (b, ′′)
This deriver, Dsk, mainly operates on ground CQs, and requires the theory to be Skolemized. This means that it cannot contain existential quantification, it may however contain function symbols. To Skolemize existential rules, for each existentially quantified variable a fresh function symbol is introduced; for the CI ∃ − ⊑ ∃ this results in (, ) → (, ()), where is a unary function symbol whose argument denotes the dependency on the variable shared between the body and head of the rule. Let be the set of Skolemized rules resulting from this transformation and note that the entailments ∪ |= q(⃗) and ∪ |= q(⃗) are equivalent for CQs q(⃗) that do not use function symbols. Our deriver internally considers two kinds of formulas: 1) CQs that may use function symbols and 2) rules of the form ∀⃗.(⃗) → (⃗), where (⃗) may now contain function terms, but no further quantified variables. Since we are only interested in CQs that are entailed by ∪ , we can assume w.l.o.g. that this entailment can be shown solely using domain elements denoted by ground terms, e.g. ( (a)), which allows us to eliminate variables from most of the inferences. For example, instead of ∃′′, ′. (b, ′′) ∧ (′′, ′) in Figure 2 we now use (b, (b)) ∧ ( (b), ( (b))). Since these atoms do not share variables, in our derivation structure we mainly need to consider inferences on single atoms, which allows for more fine-grained proofs (see Figure 4). Only at the end we need to compose atoms to obtain a CQ. ⃗
The simplified inference schemas are shown in Figure 3. In (MPs), () and (⃗) are ground atoms with terms composed from individual names and Skolem functions, and likewise (⃗) 1(⃗1) ∧ · · · ∧ (⃗) 1(⃗1) . . . (⃗) (⃗, ⃗) → (⃗)
(⃗) 1(⃗1) . . . (⃗) (Cs)
(⃗) ∃⃗.(⃗) (MPs) (Es) may contain Skolem functions; similar to (MP), we require that there is a substitution such that ( (⃗, ⃗)) = { 1(⃗1), . . . , ()} and (⃗) ∈ ( (⃗)). In (Es), ⃗ is now a vector of ⃗ ground terms which may contain function symbols. Since (MPs) works only with ground atoms, (Cs) and (Es) can now only be used at the end of a proof to obtain the desired CQ (see Figure 4). Moreover, we do not need a version of (T) here since it would be trivial for ground atoms. Its efects in Dcq can be simulated here due to the fact that the same atom can be used several times as a premise for (MPs) or (Cs).
Definition 4 (Skolemized Deriver). The derivation structure Dsk( ∪ , q(⃗)) is defined similarly to Definition 3, but using and the inference schemas (MPs), (Cs) and (Es).
Though diferent presentations with diferent advantages and disadvantages, it is not hard to translate proofs based on Dsk into proofs in Dcq and vice versa.
Lemma 5. Any proof in Dcq( ∪, q(⃗)) can be transformed into a proof in Dsk( ∪, q(⃗)) in time polynomial in the sizes of and , and conversely any proof in Dsk( ∪ , q(⃗)) can be transformed into a proof in Dcq( ∪ , q(⃗)) in time polynomial in the sizes of and . The latter also holds for tree proofs.
However, it is not the case that minimal proofs are equivalent for these two derivers, i.e. a minimal proof may become non-minimal after the transformation.
This lemma also shows that our derivation structures are complete, i.e. if ∪ |= q(⃗) holds, then we can provide a proof for it. To see this, consider the minimal Herbrand model of ∪, which can be computed using the (Skolem) chase procedure for existential rules—essentially, applying the rules step-by-step to obtain new ground atoms, in a way very similar to (MPs). This model is a universal model for CQ answering over ∪ , which means that ∪ |= q(⃗) implies |= q(⃗), which, in turn, means that there must be a proof in Dsk( ∪ , q(⃗)), and hence by Lemma 5 also one in Dcq( ∪ , q(⃗)). For convenience, we assume in the following that TBoxes are silently Skolemized when constructing derivation structures using Dsk, that is, we identify Dsk( ∪ , q(⃗)) with Dsk( ∪ , q(⃗)).
It is our intution that proofs in Dsk are more comprehensible than in Dcq because of its simpler
labels. Moreover, we assume small proofs (w.r.t. size ms or tree size mt) to be more
comprehensible than large ones (but one can certainly also consider other measures [
(MPs)
( (b), ( (b)))
we now study the complexity of finding small proofs automatically (which is independent of the
comprehensibility of the resulting proofs). More precisely, we are interested in the following
decision problem OPx(ℒ, m) for a deriver Dx ∈ {Dcq, Dsk}, a DL ℒ ∈ {ℰℒ, DL-Lite}, and
a measure m ∈ {ms, mt}: given an ℒ-KB ∪ , a query q(⃗) with certain answer ⃗, and a
natural number (in binary encoding), is there a proof for q(⃗) in Dx( ∪ , q(⃗)) with
m( ) ≤ ? To better distinguish the complexity of finding small proofs from that of query
answering, we assume ∪ |= q(⃗) as prerequisite, which fits the intuition that users request
an explanation only after they know that ⃗ is a certain answer. Lemma 7 in [
It is common in the context of OMQA to distinguish between data complexity, where only the data varies, and combined complexity, where also the influence of the other inputs is taken into account. This raises the question whether the bound is seen as part of the input or not. It turns out that fixing trivializes the data complexity, because then also fixes the set of relevant ABoxes modulo isomorphism.
Theorem 6. For a constant bound , OPx(ℒ, m) is in AC0 in data complexity.
One may argue that, since the size of the proof depends on , the bound on the proof size should be considered part of the data as well. Under this assumption, our decision problem is not necessarily in AC0 anymore. For example, consider the ℰℒ TBox {∃. ⊑ } and () ← (). For every , there is an ABox such that () is entailed by a seqeuence of role assertions, and thus needs a proof of size at least . Deciding whether this query admits a bounded proof is thus as hard as deciding whether it admits an answer at all in , i.e. P-hard [27]. However, we at least stay in AC0 for DLs over which CQs are rewritable, e.g. DL-Lite [24], because the number of (non-isomorphic) proofs that we need to consider is bounded by the size of the rewriting, which is constant in data complexity.
Theorem 7. If all CQs are UCQ-rewritable over ℒ-TBoxes, then OPx(ℒ, m) is in AC0 in data complexity.
We now consider the combined complexity. In [
A direct consequence of Lemmas 5 and 8 is the upper bound in the following theorem. The lower bound can be shown by a reduction from Boolean query entailment over DL-Lite ontologies: for this, we extend the KB in a given query answering problem by axioms that trivially entail the query, but only yield proofs larger than .
Theorem 9. OPx(DL-Lite, m) is NP-complete.
To obtain tractability, we can restrict the shape of the query. Recall that the Gaifman graph of a query q is the undirected graph using the terms of q as nodes and has an edge between terms occurring together in an atom. A query is tree-shaped if its Gaifman graph is a tree. Theorem 10. Given a DL-Lite KB ∪ and a tree-shaped CQ q(⃗) with certain answer ⃗, one can compute in polynomial time a proof of minimal tree size in Dsk( ∪ , q(⃗)).
The central property used in the proof of Theorem 10 is that for tree size every atom in q(⃗) has a separate proof, even if two atoms are proven in the same way. To avoid this redundancy, one could think about modifying (Es) slightly:
(⃗) ∃⃗.′(⃗)
(E′s) , provided there exists : ⃗ → ⃗ s.t. ′(⃗) = (⃗) Denote the resulting deriver by D′sk. Using (E′s), we can derive ∃, . () ∧ () from (); with (Es), the premise would need to be () ∧ (). However, this modification is already suficient to make our problem NP-hard for tree-shaped queries, even without a TBox. The same problem arises in Dcq (where atoms can be duplicated using (T)), and if we consider ms. Theorem 11. For tree-shaped CQs, OP′x(ℒ, mt) is NP-hard. The same holds for OPsk(ℒ, ms) and OPcq(ℒ, mt).
We now consider proofs for temporal query answering. In this setting, TBox axioms hold globally, i.e. at all time points, the ABox contains information about the state of the world in diferent time intervals, and the query contains (metric) temporal operators.
An interval is a nonempty subset of Z of the form [1, 2], where 1, 2 ∈ Z ∪ {∞} and 1 ≤ 2 (for simplicity, we write [∞, 2] for (−∞ , 2] and [1, ∞] instead of [1, ∞));2 1 and 2 are encoded in binary. A temporal ABox is a finite set of facts of the form ()@ or (, )@ , where () and (, ) are assertions and is an interval. The fact ()@ states that () holds throughout the interval . We denote by tem() the multiset of intervals that occur in and |tem()| is the sum of their lengths. A temporal interpretation I = (ΔI, (ℐ)∈Z), is a collection of DL interpretations ℐ = (ΔI, · ℐ ), ∈ Z, over ΔI. I satisfies a TBox axiom if each ℐ, ∈ Z, satisfies , and it satisfies a temporal assertion @ if each ℐ, ∈ , satisfies .
We use the finite-range positive version of metric temporal conjunctive queries (MTCQs) introduced in [29, 30], combining CQs with MTL operators [31, 32, 33].
Definition 12.
An MTCQ is of the form q(⃗, ) = (⃗)@, where is built according to
::= | ⊤ | ∧ | ∨ | ⊟ | ⊞ | | , with an interval variable, a CQ, a finite interval with non-negative endpoints, and ⃗ the free variables of all CQs in . A certain answer to q(⃗, ) over ∪ is a pair (⃗, ) such that ⃗ ⊆ ind(), is an interval and, for any ∈ and any model I of ∪ , we have I, |= (⃗) according to Table 1. We denote this as ∪ |= q(⃗, ).
For temporal extensions of Definitions 3 and 4, we will interpret ⊑ ′ now as the global temporal rule () → ′() holding in any possible interval.
(⃗, ⃗) → ∃⃗. (⃗, ⃗) (∃⃗. (⃗))@ (TMP)
Similarly, we need temporal versions of (C) and (E), where all CQs are annotated with the same interval variable. In addition, we need an inference for disjunctive MTCQS:
To provide a proof for a temporal query, we need to be able to coalesce, i.e. merge intervals: ∃⃗1. (⃗1)@ 1 . . .
(∃⃗. (⃗))@ ⋃︀ =1 ∃⃗. (⃗)@ (COAL) where ⋃︀
=1 is a single interval and (⃗1), . . . , (⃗) are identical up to variable renaming. On the other hand, we also need an inverse operation to shrink intervals: (SEP) where ′ ⊆ . Both inferences are needed to infer all intervals with ∪ |= ∃⃗. (⃗)@ .
Finally, we need inferences for the temporal operators, where for [1,2] we only consider the case where 1 > 0 since [0,2] is equivalent to ∨ ( [1,2] ): ⊞ [1,2](⃗)@[1 − 1, 2 − 2] (⊞ ) (⃗)@ (⃗) [1,2] (⃗)@( − [1, 2]) ∩ ( ) where := ( + 1) ∩ ′ (all time points where -s are immediately preceded by -s) and [1, 2] − [1, 2] := [1 − 2, 2 − 1], and none of the involved intervals should be empty. Inferences for ⊟ and are similar. We denote the resulting deriver by Dtcq. A Skolemized variant Dtsk can be defined similarly with temporalized versions of (MPs), (Cs), and (Es). We can now lift Theorems 7 and 9 to this setting.
Theorem 13. If CQ answering in ℒ is UCQ-rewritable, then MTCQ answering is also UCQrewritable and OPtx(ℒ, m) is in AC0 in data complexity. Moreover, OPtx(DL-Lite, m) is NPcomplete. Let D ∈ {Dtcq, Dtsk}. Then, it is NP-complete to decide whether, given a DL-Lite TBox , a temporal ABox , q(⃗, ) s.t. ∪ |= q(⃗, ), and in unary or binary encoding, there exists a proof in D( ∪ , q(⃗, )) of (tree) size at most .
We started to explore a framework for proofs of answers to conjunctive queries. In the future,
we want to extend our complexity results to other DLs, and our framework to DLs that cannot
be translated to existential rules. Other interesting research questions include derivers that
combine TBox and query entailment rules, e.g. Dcq plus the rules of the ELK reasoner [34].
Instead of proofs, one could also try to show a canonical model to a user in order to explain
query answers. For explaining missing answers, we also want to continue investigating how to
ifnd (optimal) counter-interpretations or abduction results [
This work was supported by DFG in grant 389792660, TRR 248 (https://perspicuous-computing. science), and QuantLA, GRK 1763 (https://lat.inf.tu-dresden.de/quantla). 24963/ijcai.2021/266. [13] İ. İ. Ceylan, T. Lukasiewicz, E. Malizia, C. Molinaro, A. Vaicenavicius, Explanations for negative query answers under existential rules, in: D. Calvanese, E. Erdem, M. Thielscher (Eds.), Proceedings of KR 2020, AAAI Press, 2020, pp. 223–232. URL: https://doi.org/10. 24963/kr.2020/23. doi:10.24963/kr.2020/23. [14] D. Calvanese, M. Ortiz, M. Simkus, G. Stefanoni, The complexity of explaining negative query answers in dl-lite, in: G. Brewka, T. Eiter, S. A. McIlraith (Eds.), Principles of Knowledge Representation and Reasoning: Proceedings of the Thirteenth International Conference, KR 2012, AAAI Press, 2012. URL: http://www.aaai.org/ocs/index.php/KR/ KR12/paper/view/4537. [15] C. Alrabbaa, W. Hieke, A. Turhan, Counter model transformation for explaining nonsubsumption in EL, in: C. Beierle, M. Ragni, F. Stolzenburg, M. Thimm (Eds.), Proceedings of the 7th Workshop on Formal and Cognitive Reasoning, volume 2961 of CEUR Workshop Proceedings, CEUR-WS.org, 2021, pp. 9–22. URL: http://ceur-ws.org/Vol-2961/paper_2.pdf. [16] D. Calvanese, D. Lanti, A. Ozaki, R. Peñaloza, G. Xiao, Enriching ontology-based data access with provenance, in: S. Kraus (Ed.), Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, ijcai.org, 2019, pp. 1616–1623. doi:10.24963/ijcai.2019/224. [17] C. Bourgaux, A. Ozaki, R. Peñaloza, L. Predoiu, Provenance for the description logic elhr, in: C. Bessiere (Ed.), Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI 2020, ijcai.org, 2020, pp. 1862–1869. doi: 10.24963/ijcai. 2020/258. [18] A. Borgida, D. Calvanese, M. Rodriguez-Muro, Explanation in the DL-Lite family of description logics, in: R. Meersman, Z. Tari (Eds.), On the Move to Meaningful Internet Systems: OTM 2008, volume 5332 of Lecture Notes in Computer Science, Springer, 2008, pp. 1440–1457. doi:10.1007/978-3-540-88873-4_35. [19] G. Stefanoni, Explaining query answers in lightweight ontologies, Diploma thesis, Technische Universität Wien, 2011. URL: http://www.cs.ox.ac.uk/files/7942/thesis.pdf. [20] F. Croce, M. Lenzerini, A framework for explaining query answers in DL-Lite, in: C. FaronZucker, C. Ghidini, A. Napoli, Y. Toussaint (Eds.), Knowledge Engineering and Knowledge Management - 21st International Conference, EKAW 2018, volume 11313 of Lecture Notes in Computer Science, Springer, 2018, pp. 83–97. doi:10.1007/978-3-030-03667-6_6. [21] C. Alrabbaa, F. Baader, R. Dachselt, T. Flemisch, P. Koopmann, Visualising proofs and the modular structure of ontologies to support ontology repair, in: S. Borgwardt, T. Meyer (Eds.), Proceedings of the 33rd International Workshop on Description Logics (DL 2020), volume 2663 of CEUR Workshop Proceedings, CEUR-WS.org, 2020. URL: http://ceur-ws.org/ Vol-2663/paper-2.pdf. [22] A. Calì, G. Gottlob, T. Lukasiewicz, A general datalog-based framework for tractable query answering over ontologies, J. Web Semant. 14 (2012) 57–83. doi:10.1016/j.websem. 2012.03.001. [23] C. Alrabbaa, S. Borgwardt, P. Koopmann, A. Kovtunova, Finding good proofs for answers to conjunctive queries mediated by lightweight ontologies (technical report), 2022. URL: https://arxiv.org/abs/2206.09758. doi:10.48550/ARXIV.2206.09758. [24] D. Calvanese, G. De Giacomo, D. Lembo, M. Lenzerini, R. Rosati, Tractable reasoning and eficient query answering in description logics: The DL-Lite family, J. of Automated Reasoning 39 (2007) 385–429. doi:10.1007/s10817-007-9078-x. [25] F. Baader, Terminological cycles in a description logic with existential restrictions, in: G. Gottlob, T. Walsh (Eds.), IJCAI-03, Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence, Morgan Kaufmann, 2003, pp. 325–330. URL: http: //ijcai.org/Proceedings/03/Papers/048.pdf. [26] R. Fagin, P. G. Kolaitis, R. J. Miller, L. Popa, Data exchange: semantics and query answering,
Theor. Comput. Sci. 336 (2005) 89–124. doi:10.1016/j.tcs.2004.10.033. [27] R. Rosati, On conjunctive query answering in EL, in: D. Calvanese, E. Franconi, V. Haarslev, D. Lembo, B. Motik, A. Turhan, S. Tessaris (Eds.), Proceedings of the 2007 International Workshop on Description Logics (DL2007), volume 250 of CEUR Workshop Proceedings, CEUR-WS.org, 2007. URL: http://ceur-ws.org/Vol-250/paper_83.pdf. [28] G. Gottlob, S. Kikot, R. Kontchakov, V. V. Podolskii, T. Schwentick, M. Zakharyaschev, The price of query rewriting in ontology-based data access, Artif. Intell. 213 (2014) 42–59. doi:10.1016/j.artint.2014.04.004. [29] S. Borgwardt, W. Forkel, A. Kovtunova, Finding new diamonds: Temporal minimalworld query answering over sparse ABoxes, in: Proc. of the 3rd Int. Joint Conf. on Rules and Reasoning, RuleML+RR 2019, volume 11784 of LNCS, Springer, 2019, pp. 3–18. doi:10.1007/978-3-030-31095-0_1. [30] S. Borgwardt, W. Forkel, A. Kovtunova, Temporal minimal-world query answering over sparse ABoxes, Theory Pract. Log. Program. 22 (2022) 193–228. URL: https://doi.org/10. 1017/S1471068421000119. doi:10.1017/S1471068421000119. [31] R. Alur, T. A. Henzinger, A really temporal logic, J. ACM 41 (1994) 181–204. doi:10.1145/ 174644.174651. [32] V. Gutiérrez-Basulto, J. C. Jung, A. Ozaki, On metric temporal description logics, in: Proc.
ECAI, IOS Press, 2016, pp. 837–845. doi:10.3233/978-1-61499-672-9-837. [33] F. Baader, S. Borgwardt, P. Koopmann, A. Ozaki, V. Thost, Metric temporal description logics with interval-rigid names, in: Proc. of the 11th Int. Symp. on Frontiers of Combining Systems (FroCoS’17), Springer, 2017, pp. 60–76. doi:10.1007/978-3-319-66167-4_4. [34] Y. Kazakov, M. Krötzsch, F. Simancik, The incredible ELK - From polynomial procedures to eficient reasoning with ℰℒ ontologies, J. Autom. Reason. 53 (2014) 1–61. doi:10.1007/ s10817-013-9296-3.