Finding Good Proofs for Answers to Conjunctive Queries Mediated by Lightweight Ontologies Christian Alrabbaa, Stefan Borgwardt, Patrick Koopmann and Alisa Kovtunova Institute of Theoretical Computer Science, Technische Universitรคt Dresden, 01062 Dresden, Germany Abstract 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 different 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. 1. Introduction Explaining description logic (DL) reasoning has a long tradition, starting with the first works on proofs for standard DL entailments [1, 2]. A popular and very effective method is justifications, which simply point out the axioms from an ontology that are responsible for an entailment [3, 4, 5, 6]. More recently, work has resumed on techniques to find proofs for explaining more complex logical consequences [7, 8, 9, 10, 11]. On the other hand, if a desired entailment does not hold, one needs different explanation techniques such as abduction [12, 13, 14] or counterinterpretations [15]. Explaining answers to conjunctive queries (CQs) has also been investigated before, in the form of abduction for missing answers over DL-Lite ontologies [14], provenance for positive answers in DL-Lite and โ„ฐโ„’ [16, 17], as well as proofs for DL-Lite query answering [18, 19, 20]. 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 [9]. There, proofs are formalized as directed, acyclic hypergraphs and DL 2022: 35th International Workshop on Description Logics, August 7โ€“10, 2022, Haifa, Israel " christian.alrabbaa@tu-dresden.de (C. Alrabbaa); stefan.borgwardt@tu-dresden.de (S. Borgwardt); patrick.koopmann@tu-dresden.de (P. Koopmann); alisa.kovtunova@tu-dresden.de (A. Kovtunova)  0000-0002-2925-1765 (C. Alrabbaa); 0000-0003-0924-8478 (S. Borgwardt); 0000-0001-5999-2583 (P. Koopmann); 0000-0001-9936-0943 (A. Kovtunova) ยฉ 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CEUR Workshop Proceedings http://ceur-ws.org ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org) proof quality can be measured in different ways. We mainly consider the size (the number of formulas) of a proof as well as its tree size, which corresponds to the size when the proof is presented in a tree-shaped way (which may require repeating subproofs), as it is often done in practice [8, 21]. The quest for good proofs is formalized as a search problem in a so-called derivation structures produced by a deriver, which specifies the possible inferences. In this paper, we consider two different 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. 2. Preliminaries Proofs In our setting, a logic โ„’ = (๐’ฎโ„’ , |=โ„’ ) consists of a set ๐’ฎโ„’ of โ„’-sentences and a con- sequence 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 [9, 10, 11], we view proofs as directed hypergraphs (see the appendix for details). Definition 1 (Derivation Structure). A derivation structure ๐’Ÿ = (๐‘‰, ๐ธ, โ„“) over a theory ๐’ฐ is a directed, labeled hypergraph that is โ€ข grounded, i.e. every leaf ๐‘ฃ in ๐’Ÿ is labeled by โ„“(๐‘ฃ) โˆˆ ๐’ฐ; and โ€ข sound, i.e. for every hyperedge (๐‘†, ๐‘‘) โˆˆ ๐ธ, the entailment {โ„“(๐‘ ) | ๐‘  โˆˆ ๐‘†} |= โ„“(๐‘‘) holds. We call hyperedges (๐‘†, ๐‘‘) โˆˆ ๐ธ inferences or inference steps, with ๐‘† being the premises and ๐‘‘ the conclusion, and may write them like ๐‘ ๐‘โ†’๐‘ž ๐‘ ๐‘โ†’๐‘ž ๐‘ž or ๐‘ž Proofs are special derivation structures that derive a goal sentence. 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 ๐’ซ [11]. The depth of ๐’ซ is the length of the longest path from a leaf to the sink (see appendix). 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๐‘… . 1 Since 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 different ways to explain this inference (see Figures 2 and 4). 3. Derivation Structures for Certain Answers 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 [9, 10, 11], we considered derivers based on the inference schemas used by a consequence-based reasoner. To obtain proofs for CQ entailment, we follow the ideas of chase procedures that replace atoms in CQs by other atoms by โ€œapplyingโ€ rules to them [26, 22, 24, 18]. We will introduce two derivers that represent different paradigms of what constitutes a proof. 3.1. The CQ Deriver 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 in- ference 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) โ€ฒ (C) โˆƒ๐‘ค โƒ— .๐œŒ(๐‘ค โƒ—) โˆƒ๐‘ฅ โƒ— โ€ฒ) โƒ— ) โˆง ๐œ“(๐‘ฆ โƒ— , โƒ—๐‘ฆ .๐œ‘(๐‘ฅ (T) โˆƒ๐‘ฅ โƒ— . ๐œ‘(๐‘ฅ โƒ— , โƒ—๐‘Ž) โƒ— , โƒ—๐‘ฆ ) โ†’ โˆƒ๐‘ฅ ๐œ‘(๐‘ฅ โƒ— . ๐œ‘(๐‘ฅ โƒ— , โƒ—๐‘ฆ ) (E) โˆƒ๐‘ฅ โƒ— , โƒ—๐‘ฆ . ๐œ‘(๐‘ฅ โƒ— , โƒ—๐‘ฆ ) Figure 1: Inference schemas for Dcq . (MP) and (T) refer to modus ponens and tautology. 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. 3.2. Skolemized Derivation Structure 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 affecting 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]. (MP) ๐ต(b) ๐ต โŠ‘ โˆƒ๐‘ƒ โˆƒ๐‘ฅโ€ฒโ€ฒ . ๐‘ƒ (b, ๐‘ฅโ€ฒโ€ฒ ) (MP) โˆƒ๐‘ƒ โˆ’ โŠ‘ โˆƒ๐‘† ๐‘ƒ โŠ‘ ๐‘…โˆ’ (MP) โˆƒ๐‘ฅโ€ฒโ€ฒ , ๐‘ง โ€ฒ ๐‘ƒ (b, ๐‘ฅโ€ฒโ€ฒ ) โˆง ๐‘†(๐‘ฅโ€ฒโ€ฒ , ๐‘ง โ€ฒ ) โˆƒ๐‘ฅโ€ฒโ€ฒ , ๐‘ง โ€ฒ . ๐‘…(๐‘ฅโ€ฒโ€ฒ , b) โˆง ๐‘†(๐‘ฅโ€ฒโ€ฒ , ๐‘ง โ€ฒ ) โˆง ๐‘ƒ (b, ๐‘ฅโ€ฒโ€ฒ ) (MP) โˆƒ๐‘…โˆ’ โŠ‘ โˆƒ๐‘‡ (T) โˆƒ๐‘ฅโ€ฒโ€ฒ , ๐‘ง, ๐‘ง โ€ฒ . ๐‘…(๐‘ฅโ€ฒโ€ฒ , b) โˆง ๐‘‡ (b, ๐‘ง) โˆง ๐‘†(๐‘ฅโ€ฒโ€ฒ , ๐‘ง โ€ฒ ) โˆง ๐‘ƒ (b, ๐‘ฅโ€ฒโ€ฒ ) ๐‘…(๐‘ฅ, ๐‘ฆ) โˆง ๐‘‡ (๐‘ฆ, ๐‘ง) โ†’ โˆƒ๐‘ฆ . ๐‘…(๐‘ฅ, ๐‘ฆ โ€ฒ ) โˆง ๐‘‡ (๐‘ฆ โ€ฒ , ๐‘ง) โ€ฒ (MP) (T) โˆƒ๐‘ฅ , ๐‘ฆ , ๐‘ง, ๐‘ง . ๐‘…(๐‘ฅ , b) โˆง ๐‘‡ (b, ๐‘ง) โˆง ๐‘‡ (๐‘ฆ โ€ฒ , ๐‘ง) โˆง ๐‘…(๐‘ฅโ€ฒโ€ฒ , ๐‘ฆ โ€ฒ ) โˆง . . . โ€ฒโ€ฒ โ€ฒ โ€ฒ โ€ฒโ€ฒ ๐‘†(๐‘ฅ, ๐‘ง) โ†’ ๐‘†(๐‘ฅ, ๐‘ง) (MP) (T) ... ๐‘…(๐‘ฅโ€ฒโ€ฒ , ๐‘ฆ โ€ฒ ) โˆง ๐‘†(๐‘ฅโ€ฒโ€ฒ , ๐‘ง โ€ฒ ) โ†’ โˆƒ๐‘ฅโ€ฒ . ๐‘…(๐‘ฅโ€ฒ , ๐‘ฆ โ€ฒ ) โˆง ๐‘†(๐‘ฅโ€ฒ , ๐‘ง โ€ฒ ) (MP) (T) ๐‘…(๐‘ฅโ€ฒโ€ฒ , ๐‘ฆ) โ†’ โˆƒ๐‘ฅ. ๐‘…(๐‘ฅ, ๐‘ฆ) (MP) ... โˆƒ๐‘ฅ, ๐‘ฅโ€ฒ , ๐‘ฅโ€ฒโ€ฒ , ๐‘ฆ โ€ฒ , ๐‘ง, ๐‘ง โ€ฒ . ๐‘…(๐‘ฅ, b) โˆง ๐‘‡ (b, ๐‘ง) โˆง ๐‘‡ (๐‘ฆ โ€ฒ , ๐‘ง) โˆง ๐‘…(๐‘ฅโ€ฒ , ๐‘ฆ โ€ฒ ) โˆง ๐‘†(๐‘ฅโ€ฒ , ๐‘ง โ€ฒ ) โˆง ๐‘†(๐‘ฅโ€ฒโ€ฒ , ๐‘ง โ€ฒ ) โˆง ๐‘ƒ (b, ๐‘ฅโ€ฒโ€ฒ ) (E) โˆƒ๐‘ฅ, ๐‘ฅโ€ฒ , ๐‘ฅโ€ฒโ€ฒ , ๐‘ฆ, ๐‘ฆ โ€ฒ , ๐‘ง, ๐‘ง โ€ฒ . ๐‘…(๐‘ฅ, ๐‘ฆ) โˆง ๐‘‡ (๐‘ฆ, ๐‘ง) โˆง ๐‘‡ (๐‘ฆ โ€ฒ , ๐‘ง) โˆง ๐‘…(๐‘ฅโ€ฒ , ๐‘ฆ โ€ฒ ) โˆง ๐‘†(๐‘ฅโ€ฒ , ๐‘ง โ€ฒ ) โˆง ๐‘†(๐‘ฅโ€ฒโ€ฒ , ๐‘ง โ€ฒ ) โˆง ๐‘ƒ (b, ๐‘ฅโ€ฒโ€ฒ ) Figure 2: A CQ proof for Example 1 (inferences (E) and (T) are delayed to the last steps) 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 (๐‘ก ... โƒ—๐‘› ) ๐œ“(๐‘ฆ ๐›ผ๐‘› (๐‘ก โƒ— , โƒ—๐‘ง ) โ†’ ๐œ’(๐‘ง โƒ—) (MPs ) ๐›ฝ(๐‘ โƒ—) โƒ—1 ) . . . ๐›ผ๐‘› (๐‘ก ๐›ผ1 (๐‘ก โƒ—๐‘› ) โƒ—) ๐œ‘(๐‘ก (Cs ) (Es ) โƒ— โƒ— ๐›ผ1 (๐‘ก1 ) โˆง ยท ยท ยท โˆง ๐›ผ๐‘› (๐‘ก๐‘› ) โˆƒ๐‘ฅ โƒ— .๐œ‘(๐‘ฅ โƒ—) Figure 3: Inference schemas for Dsk . 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 effects 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 different presentations with different 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(๐‘Ž โƒ— )). 4. The Complexity of Finding Good Proofs 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 comprehen- sible than large ones (but one can certainly also consider other measures [10, 11]). Therefore, (MPs ) ๐ต(b) ๐ต โŠ‘ โˆƒ๐‘ƒ (MPs ) (MPs ) ๐‘ƒ โŠ‘ ๐‘…โˆ’ ๐‘ƒ (b, ๐‘“ (b)) โˆƒ๐‘ƒ โˆ’ โŠ‘ โˆƒ๐‘† (MPs ) โˆƒ๐‘…โˆ’ โŠ‘ โˆƒ๐‘‡ ๐‘…(๐‘“ (b), b) ๐‘†(๐‘“ (b), ๐‘”(๐‘“ (b))) ๐‘‡ (b, โ„Ž(b)) (Cs ) ๐‘…(๐‘“ (b), b) โˆง ๐‘‡ (b, โ„Ž(b)) โˆง ๐‘‡ (b, โ„Ž(b)) โˆง ๐‘…(๐‘“ (b), b) โˆง ๐‘†(๐‘“ (b), ๐‘”(๐‘“ (b))) โˆง ๐‘†(๐‘“ (b), ๐‘”(๐‘“ (b))) โˆง ๐‘ƒ (b, ๐‘“ (b)) (Es ) โˆƒ๐‘ฅ, ๐‘ฅโ€ฒ , ๐‘ฅโ€ฒโ€ฒ , ๐‘ฆ, ๐‘ฆ โ€ฒ , ๐‘ง, ๐‘ง โ€ฒ . ๐‘…(๐‘ฅ, ๐‘ฆ) โˆง ๐‘‡ (๐‘ฆ, ๐‘ง) โˆง ๐‘‡ (๐‘ฆ โ€ฒ , ๐‘ง) โˆง ๐‘…(๐‘ฅโ€ฒ , ๐‘ฆ โ€ฒ ) โˆง ๐‘†(๐‘ฅโ€ฒ , ๐‘ง โ€ฒ ) โˆง ๐‘†(๐‘ฅโ€ฒโ€ฒ , ๐‘ง โ€ฒ ) โˆง ๐‘ƒ (b, ๐‘ฅโ€ฒโ€ฒ ) Figure 4: A Skolemized proof for Example 1 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 [11] shows that, instead of looking for arbitrary proofs and homomorphisms into the derivation structure, one can restrict the search to subproofs of Dx (๐’ฏ โˆช ๐’œ, q(๐‘Ž โƒ— )), which we will often do implicitly. 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 [9, 11], we established general upper bounds for finding proofs of bounded size. These results depend only on the size of the derivation structure obtained for the given input. Both Dcq and Dsk may produce derivation structures of infinite size, as Dcq contains CQs of arbitrary size, and Dsk also has Skolem terms of arbitrary nesting depth. However, we can sometimes bound the number of relevant Skolem terms in Dsk by considering only the part of the minimal Herbrand model ๐ป that is necessary to satisfy the query q(๐‘Ž โƒ— ). For example, in logics with the polynomial witness property [28], including DL-Lite๐‘… , we know that any query that is entailed is already satisfied after polynomially many chase steps used to construct ๐ป. In particular, this means that the nesting depth of Skolem terms in a proof is bounded polynomially (in the size of the TBox and the query), and hence the part of Dsk (๐’ฏ ๐‘  โˆช ๐’œ, q(๐‘Ž โƒ— )) that we need to search for a (small) proof is bounded exponentially. For such structures, our results from [9, 11] give us a NExpTime-upper bound for size, and a PSpace-upper bound for tree size, upon which we can improve with the following lemma. Lemma 8. There is a polynomial ๐‘ such that for any DL-Lite๐‘… KB ๐’ฏ โˆช ๐’œ, CQ q(๐‘ฅ โƒ— ), and certain answer โƒ—๐‘Ž, there is a proof in Dsk (๐’ฏ โˆช ๐’œ, q(๐‘Ž โƒ— )) of tree size at most ๐‘(|๐’ฏ |, |q(๐‘ฅ โƒ— )|). 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 sufficient 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 ). Table 1 Semantics of (Boolean) MTCQs for I = (ฮ”I , (โ„๐‘– )๐‘–โˆˆZ ) and ๐‘– โˆˆ Z. ๐œ‘ I, ๐‘– |= ๐œ‘ iff CQ ๐œ“ โ„๐‘– |= ๐œ“ โŠค true ๐œ‘โˆง๐œ“ I, ๐‘– |= ๐œ‘ and I, ๐‘– |= ๐œ“ ๐œ‘โˆจ๐œ“ I, ๐‘– |= ๐œ‘ or I, ๐‘– |= ๐œ“ โŠž๐ผ ๐œ‘ โˆ€๐‘˜ โˆˆ ๐ผ such that I, ๐‘– + ๐‘˜ |= ๐œ‘ โŠŸ๐ผ ๐œ‘ โˆ€๐‘˜ โˆˆ ๐ผ such that I, ๐‘– โˆ’ ๐‘˜ |= ๐œ‘ ๐œ‘ ๐’ฐ๐ผ ๐œ“ โˆƒ๐‘˜ โˆˆ ๐ผ such that I, ๐‘–+๐‘˜ |= ๐œ“ and โˆ€๐‘— : 0 โ‰ค ๐‘— < ๐‘˜ : I, ๐‘–+๐‘— |= ๐œ‘ ๐œ‘ ๐’ฎ๐ผ ๐œ“ โˆƒ๐‘˜ โˆˆ ๐ผ such that I, ๐‘–โˆ’๐‘˜ |= ๐œ“ and โˆ€๐‘— : 0 โ‰ค ๐‘— < ๐‘˜ : I, ๐‘–โˆ’๐‘— |= ๐œ‘ 5. Metric Temporal CQs 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 different 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 โƒ— , ๐‘ค) over ๐’ฏ โˆช ๐’œ is a pair (๐‘Ž free variables of all CQs in ๐œ‘. A certain answer to q(๐‘ฅ โƒ— , ๐œ„) 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: 2 This allows us to avoid considering special cases in the interval arithmetic below. ๐œ‘(๐‘ฅ โƒ— )@๐œ„ (DISJ) โƒ— ) โˆจ ๐œ“(๐‘ฆ (๐œ‘(๐‘ฅ โƒ— ))@๐œ„ To provide a proof for a temporal query, we need to be able to coalesce, i.e. merge intervals: โˆƒ๐‘ฅ โƒ— 1 . ๐œ‘(๐‘ฅ โƒ— 1 )@๐œ„1 ... โˆƒ๐‘ฅ โƒ— ๐‘› . ๐œ‘(๐‘ฅ โƒ— ๐‘› )@๐œ„๐‘› โ‹ƒ๏ธ€๐‘› (COAL) (โˆƒ๐‘ฅ โƒ— . ๐œ‘(๐‘ฅ โƒ— ))@ ๐‘–=1 ๐œ„๐‘– 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 ] ๐œ“(๐‘ฆ ๐œ‘(๐‘ฅ โƒ— )@(๐œˆ โˆ’ [๐‘Ÿ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 UCQ- rewritable and OPtx (โ„’, m) is in AC0 in data complexity. Moreover, OPtx (DL-Lite๐‘… , m) is NP- complete. 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 ๐‘›. 6. Conclusion 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 find (optimal) counter-interpretations or abduction results [12]. Acknowledgments 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). References [1] D. L. McGuinness, Explaining Reasoning in Description Logics, Ph.D. thesis, Rutgers University, NJ, USA, 1996. doi:10.7282/t3-q0c6-5305. [2] A. Borgida, E. Franconi, I. Horrocks, Explaining ๐’œโ„’๐’ž subsumption, in: ECAI 2000, Proceedings of the 14th European Conference on Artificial Intelligence, 2000, pp. 209โ€“213. URL: http://www.frontiersinai.com/ecai/ecai2000/pdf/p0209.pdf. [3] S. Schlobach, R. Cornet, Non-standard reasoning services for the debugging of description logic terminologies., in: G. Gottlob, T. Walsh (Eds.), Proc. of the 18th Int. Joint Conf. on Artificial Intelligence (IJCAI 2003), Morgan Kaufmann, 2003, pp. 355โ€“362. URL: http: //ijcai.org/Proceedings/03/Papers/053.pdf. [4] F. Baader, R. Peรฑaloza, B. Suntisrivaraporn, Pinpointing in the description logic โ„ฐโ„’+ , in: KI 2007: Advances in Artificial Intelligence, 30th Annual German Conference on AI, KI 2007, 2007, pp. 52โ€“67. doi:10.1007/978-3-540-74565-5_7. [5] R. Peรฑaloza, Axiom-Pinpointing in Description Logics and Beyond, Ph.D. thesis, Technis- che Universitรคt Dresden, Germany, 2009. URL: https://nbn-resolving.org/urn:nbn:de:bsz: 14-qucosa-24743. [6] M. Horridge, Justification Based Explanation in Ontologies, Ph.D. thesis, University of Manchester, UK, 2011. URL: https://www.research.manchester.ac.uk/portal/files/54511395/ FULL_TEXT.PDF. [7] M. Horridge, B. Parsia, U. Sattler, Justification oriented proofs in OWL, in: The Semantic Web - ISWC 2010 - 9th International Semantic Web Conference, ISWC 2010, Part I, 2010, pp. 354โ€“369. doi:10.1007/978-3-642-17746-0_23. [8] Y. Kazakov, P. Klinov, A. Stupnikov, Towards reusable explanation services in protege, in: A. Artale, B. Glimm, R. Kontchakov (Eds.), Proc. of the 30th Int. Workshop on Description Logics (DLโ€™17), volume 1879 of CEUR Workshop Proceedings, 2017. URL: http://www. ceur-ws.org/Vol-1879/paper31.pdf. [9] C. Alrabbaa, F. Baader, S. Borgwardt, P. Koopmann, A. Kovtunova, Finding small proofs for description logic entailments: Theory and practice, in: E. Albert, L. Kovacs (Eds.), LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 73 of EPiC Series in Computing, EasyChair, 2020, pp. 32โ€“67. doi:10. 29007/nhpp. [10] C. Alrabbaa, F. Baader, S. Borgwardt, P. Koopmann, A. Kovtunova, On the complexity of finding good proofs for description logic entailments, in: S. Borgwardt, T. Meyer (Eds.), Proceedings of the 33rd International Workshop on Description Logics (DLโ€™20), volume 2663 of CEUR Workshop Proceedings, 2020. URL: http://ceur-ws.org/Vol-2663/paper-1.pdf. [11] C. Alrabbaa, F. Baader, S. Borgwardt, P. Koopmann, A. Kovtunova, Finding good proofs for description logic entailments using recursive quality measures, in: A. Platzer, G. Sutcliffe (Eds.), Proceedings of the 28th International Conference on Automated Deduction (CADEโ€™21), volume 12699 of LNCS, 2021, pp. 291โ€“308. doi:10.1007/ 978-3-030-79876-5_17. [12] P. Koopmann, Signature-based abduction with fresh individuals and complex concepts for description logics, in: Z. Zhou (Ed.), Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, ijcai.org, 2021, pp. 1929โ€“1935. doi:10. 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 non- subsumption 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, Tech- nische 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. Faron- Zucker, 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 efficient 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 minimal- world 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 efficient reasoning with โ„ฐโ„’ ontologies, J. Autom. Reason. 53 (2014) 1โ€“61. doi:10.1007/ s10817-013-9296-3.