Horn-Rewritability vs PTime Query Evaluation in Ontology-Mediated Querying

1 Introduction

In ontology-mediated querying, description logic (DL) TBoxes are used to enrich incomplete data with domain knowledge, enabling more complete answers to queries [Poggi et al., 2008; Bienvenu and Ortiz, 2015; Kontchakov and Zakharyaschev, 2014]. For expressive DLs such as ALC or SHIQ, this results in query evaluation to be CONP-hard (in data complexity) [Schaerf, 1993; Hustadt et al., 2007; Krisnadhi and Lutz, 2007]. Consequently, identifying computationally more well-behaved setups has been an important goal of research [Calvanese et al., 2013]. In particular, this has led to the introduction of Horn-DLs, syntactically defined fragments of expressive DLs that fall within the Horn-fragment of first-order logic and enable polynomial time ontology-mediated querying, examples include Horn-ALC and Horn-SHIQ [Hustadt et al., 2007; Eiter et al., 2008; Ortiz et al., 2010; 2011]. On top of enjoying lower data complexity, Horn-DLs come with several techniques that facilitate efficient query evaluation in practice such as the chase, query rewriting, and deterministic materialization [Bienvenu and Ortiz, 2015; Kontchakov and Zakharyaschev, 2014].

In this paper, we ask the converse question: Assume that a TBox T is formulated in an expressive DL L and admits PTIME query evaluation. Does it follow that T can be replaced by a TBox T ′ formulated in the corresponding Horn-DL without affecting the answers to queries? Let us make this more precise. We concentrate on queries that are conjunctive queries (CQ) since these are widely used in ontology-mediated querying and require T and T ′ to be CQ-inseparable, that is, to give exactly the same answers to any CQ on any ABox, see [Lutz and Wolter, 2010; Botoeva et al., 2016a; 2016b]. We say that an L TBox T is CQ-Horn-rewritable if there is a TBox T ′ formulated in Horn-L that is CQ-inseparable from T . The main property of an expressive DL L that we are interested in is then whether CQ-Horn-rewritability captures PTIME query evaluation, that is, whether every L TBox that enjoys PTIME CQ-evaluation is CQ-Horn-rewritable. Note that when L satisfies this property, then for any L TBox T that enjoys PTIME CQ-evaluation one can take advantage of the algorithms available for CQevaluation w.r.t. Horn-L TBoxes, via the CQ-inseparable Horn TBox.

Seemingly natural variations of the above are obtained by requiring that T ′ is logically equivalent to T rather than CQinseparable or that it is a model-theoretic conservative extension of T . Then, however, rewritability into a Horn TBox fails already for very simple TBoxes that admit CQ-evaluation in PTIME. For example, it can be shown that the TBox T1 which states that every author is the author of a novel or a short story or of non fiction, in symbols

∃author.Short Story ⊔ ∃author.¬Fiction,

has no conservative extension that is a Horn TBox, but nevertheless enjoys CQ-evaluation in PTIME. In fact, T1 is CQinseparable from the empty TBox, which is a Horn TBox.

It turns out that whether CQ-Horn-rewritability captures PTIME query evaluation depends on various factors, in particular on whether or not the unique name assumption (UNA) is made, on the DL under consideration, and on the nesting depth of quantifiers in TBoxes. Regarding the UNA, recall that answers to ontology-mediated queries depend on whether the UNA is made whenever a DL is used that admits a form of counting such as number restrictions and functional roles. To illustrate this, consider the following TBox T2 stating that everybody who authored at least 200 publications is a prolific author:

Then, with the UNA, it clearly follows that Bob is a prolific author. Without the UNA, however, some of the individual names booki might denote the same individual, and so it does not follow that Bob is a prolific author.

Regarding the impact of the UNA on CQ-Horn-rewritability and PTIME CQ-evaluation, we first make the following fundamental observations for the expressive DL ALCHIQ, which is the main DL considered in this paper:

1. PTIME CQ-evaluation without UNA implies PTIME CQevaluation with UNA; the converse does not hold with T2 being a counterexample: one can show that CQevaluation w.r.t. T2 is in PTIME with UNA, but CONPhard without UNA.
2. CQ-Horn-rewritability (and, in fact, whether a given TBox is a CQ-Horn-rewriting) does not depend on the UNA; we can thus speak about CQ-Horn-rewritability independently from the UNA.

As stated in Point 1, T2 admits PTIME CQ-evaluation with the UNA while it is CONP-hard without. Unless PTIME = NP, T2 is thus not CQ-Horn-rewritable without the UNA. Consequently, with the UNA CQ-Horn-rewritability does not capture PTIME CQ-evaluation for ALCQ-TBoxes without quantifier nesting (depth 1 TBoxes, for short). Interestingly, concept inclusions (CIs) of the form used in T2 are very common in real-world ontologies: we analyzed the Bioportal and ORE repositories [Whetzel et al., 2011; Parsia et al., 2017] and found a total of 5081 (respectively, 6958) CIs of depth 1 that contain number restrictions of which 2066 (respectively, 1720) are provably not CQ-Hornrewritable but enjoy PTIME CQ-evaluation with the UNA. Such CIs occur in 41 (from a total of 97) and 186 (from a total of 414) ontologies with number restrictions in the Bioportal and ORE repositories.

The situation is very different without the UNA: in this case, we prove that CQ-Horn-rewritability captures PTIME query evaluation for all ALCHIQ TBoxes of depth 1. We show this by constructing from a TBox T of depth 1 a canonical Horn-TBox Thorn such that Thorn is a CQ-inseparable rewriting of T if and only if CQ-evaluation w.r.t. T without UNA is in PTIME. We also show that deciding whether an ALCHIQ TBox of depth 1 is CQ-Horn-rewritable is EXPTIME-complete. Observe that in practice the restriction to TBoxes of depth 1 is a rather minor one (more than 95% of all ontologies on the Bioportal and ORE repositories have depth 1, sometimes modulo a straightforward reformulation). In theory, however, the restriction is crucial: we show that for ALC TBoxes of depth 3, CQ-Horn-rewritability does not capture PTIME query evaluation and that for ALCF TBoxes of depth 3 CQ-Hornrewritability is undecidable.

Finally, we return to CQ-evaluation with the UNA and show that TBoxes in the fragment ALCHIF ⊑f of ALCHIF in which no functional role includes another role enjoy PTIME CQ-evaluation with the UNA iff they enjoy PTIME CQevaluation without the UNA and that without this condition the equivalence fails already for TBoxes of depth 1. We thus determine a 'maximal' fragment of ALCHIF in which CQHorn-rewritability captures PTIME query evaluation with the UNA for TBoxes of depth 1.

Related Work. Rewritability into tractable languages has been studied extensively in description logic. A large body of work investigates rewritability of ontology-mediated queries (OMQs) into FO or Datalog queries giving the same answers on all ABoxes [Bienvenu et al., 2014; 2016; Feier et al., 2017]. The main difference to the work presented in this paper is that both the TBox and the CQ are given as input whereas in this paper we quantify over all CQs. In [Kaminski et al., 2016; Kaminski and Grau, 2015; Carral et al., 2014], the authors consider Horn-DL and EL rewritability of OMQs with atomic queries. Rewritability of TBoxes in an expressive DL into logically equivalent TBoxes or conservative extensions in a weaker DLs has been investigated in [Lutz et al., 2011; Konev et al., 2016].

2 Preliminaries

We use standard notation for DLs [Baader et al., 2017]. Let NC, NR, and NI be countably infinite sets of concept, role, and individual names. A role is a role name or the inverse r- of a role name r. ALCIQ-concepts are formed according to the rule

where A ∈ NC, r is a role, and n is a non-negative integer. Concepts of the form (⩾ n r C) and (⩽ n r C) are called qualified number restrictions. An ALCIQ concept inclusion (CI) takes the form C ⊑ D, where C and D are ALCIQ-concepts. An ALCIQ TBox is a finite set of ALCIQ CIs. A role inclusion (RI) takes the form r ⊑ s, where r and s are roles. An ALCHIQ TBox T is a finite set of ALCIQ CIs and RIs. We also consider various DLs contained in ALCHIQ. ALCHI is obtained from ALCHIQ by restricting the qualified number restrictions to concepts of the form (⩾ 1 r C) (also written ∃r.C) and (⩽ 0 r C) (also written ∀r.¬C), and ALCHIF is the extension of ALCHI with functionality assertion taking the form ⊤ ⊑ (⩽ 1 r ⊤). We also use ELI concepts which are constructed using ⊤, concept names, ⊓, and ∃r.C with r a role. For any concept, CI, or TBox T , we use |T | to denote the number of symbols needed to write T assuming that numbers in number restrictions are coded in unary.

An ABox A is a non-empty finite set of assertions of the form A(a) and r(a, b) with A ∈ NC, r ∈ NR, and a, b ∈ NI. We denote by ind(A) the set of individual names occurring in A.

Interpretations I take the form (∆I , ·I ), where ∆I is the non-empty domain of I and ·I interprets every concept name A as a subset AI of ∆I , role name r as a binary relation rI in ∆I , and individual name a as an element aI of ∆I . The extension C I of a concept C in I is defined as usual. An interpretation I satisfies a CI C ⊑ D if C I ⊆ DI , an RI r ⊑ s if rI ⊆ sI , an assertion A(a) if aI ∈ AI , and an assertion r(a, b) if (aI , bI ) ∈ rI . We say that I satisfies the unique name assumption (UNA) if aI ̸= bI for all individual names a ̸= b. An interpretation I is a model of a TBox T if it satisfies all CIs and RIs in T and I is a model of an ABox A if it satisfies all assertions in A. We call an ABox A satisfiable w.r.t. a TBox T (with UNA) if A and T have a common model (satisfying the UNA).

The depth of an ALCIQ concept is the maximal number of nestings of the qualified number restrictions in it; thus (≥ 5r.A) has depth 1 and (⩾ 5 r (⩾ 4 r A)) has depth 2. The depth of a TBox, which will play an important role in this paper, is the maximal depth of the concepts that occur in it. For deciding satisfiability and subsumption, TBoxes are often normalized to depth 1 in a pre-processing step [Kazakov, 2009; Kaminski et al., 2016]. This does not work for the questions studied in this paper since normalization can change the complexity of the TBox, see [Lutz and Wolter, 2017; Hernich et al., 2017].

A Horn-ALCIQ CI takes the form L ⊑ R, where L and R are built according to the following syntax rules

A Horn-ALCHIQ TBox is a finite set of Horn-ALCIQ CIs and RIs. Note that there are several alternative ways to define Horn-DLs [Hustadt et al., 2007; Kr¨otzsch et al., 2007; Eiter et al., 2008; Kazakov, 2009]. The results in this paper apply to all these definitions: whenever we claim that a sentence cannot be expressed using a Horn-TBox, the proof establishes failure of preservation under direct products which shows that the sentence cannot be expressed in FO-Horn [Chang and Keisler, 1990; Lutz et al., 2011], and if we rewrite into a Horn-TBox we always rewrite into a TBox of depth 1 in which case all definitions of Horn-TBoxes coincide.

A conjunctive query (CQ) q(⃗x) is an FO-formula of the form ∃⃗y ϕ(⃗x, ⃗y), where ϕ(⃗x, ⃗y) is a conjunction of atoms of the form A(x), r(x, y), and x = y. Every ELI concept C defines in the natural way a tree-shaped CQ with one free variable, written C(x) [Lutz and Wolter, 2017]. Let ELIQ denote the class of all such CQs, and let ELIQ= denote the union of ELIQ and the set of all equalities x = y. We say that a tuple ⃗a of individuals in an ABox A is a certain answer to the CQ q(⃗x) over A w.r.t. a TBox T , in symbols T , A |= q(⃗a) if I |= q(⃗a) holds for all models I of T and A. The query evaluation problem for T and CQ q is the problem to decide for a given ABox A and tuple ⃗a of individuals from A, whether T , A |= q(⃗a). We say that the CQ-evaluation problem for T is in PTIME if the query evaluation problem for T and q is in PTIME for every CQ q. Note that our default assumption when speaking about query evaluation is that we do not make the UNA. If we do, then we shall always explicitly say so. We write T ,A |=UNA q(⃗a) if I |= q(⃗a) holds for all models I of T and A satisfying the UNA and the query evaluation problem for T and CQ q with the UNA is the problem to decide T ,A |=UNA q(⃗a). If we want to emphasize that we do not make the UNA, we write T , A |=nUNA q(⃗a) instead of T , A |= q(⃗a). The relationship between certain answers with and without the UNA can be expressed using the following equivalence:

It is well known that for DLs that do not admit any forms of counting the UNA does not affect the certain answers to CQs. Thus, if T is an ALCHI TBox, then T ,A |=UNA q(⃗a) iff T ,A |=nUNA q(⃗a).

In this paper, we aim to understand whether and when a TBox formulated in an expressive DL can be replaced with a TBox formulated in the corresponding Horn-DL without changing the answers to CQs. Following [Lutz and Wolter, 2010; Botoeva et al., 2016a; 2016b], TBoxes T1 and T2 are CQ-inseparable if for all CQs q, all ABoxes A, and all tuples ⃗a of individual names in A, the following equivalence holds:

If T2 is a Horn TBox, then we call T2 a CQ-Horn-rewriting of T1. A TBox T in a DL L is CQ-Horn-rewritable if there exists a CQ-Horn-rewriting of T in Horn-L. We further say that CQHorn-rewritability captures PTIME query evaluation for L if every TBox in L is CQ-Horn-rewritable. Thus, as before, by default we do not make the UNA. The notions introduced above are modified in the obvious way if one makes the UNA and we will always make this explicit.

3 Transfer between UNA and non-UNA

We investigate the influence of the UNA on CQ-Hornrewritability and the complexity of CQ-evaluation. We show that for ALCHIQ TBoxes CQ-Horn-rewritability does not depend on the UNA, but that for PTIME CQ-evaluation only one direction holds: if CQ-evaluation is in PTIME without UNA, then it is in PTIME with UNA. In the proof we use a disjunction property of TBoxes and show that it is a necessary condition for CQ-evaluation to be in PTIME, with and without UNA (unless PTIME equals CONP).

For an ABox A, CQs q1(⃗x1), . . . , qn(⃗xn), and tuples ⃗a1, . . . ,⃗an in A, we write T ,A |=nUNA ∨1≤i≤n qi(⃗ai) if for every model I of T and A there is i ∈ {1, . . . , n} with I |= qi(⃗ai), and we define T ,A |=UNA ∨1≤i≤n qi(⃗ai) accordingly based on models that satisfy the UNA. Let Q be a class of CQs. A TBox T has the Q-disjunction property without UNA if for all ABoxes A, CQs q1(⃗x1), . . . , qn(⃗xn) ∈ Q and tuples ⃗a1, . . . ,⃗an in A with T , A |=nUNA ∨1≤i≤n qi(⃗ai) there exists i ∈ {1, . . . , n} such that T ,A |= qi(⃗ai). The Q-disjunction property with UNA is defined accordingly.

Example 1. The TBox T2 from the introduction does not enjoy the ELIQ=-disjunction property without UNA, but enjoys it with UNA. To show the first claim note that for the ABox A2 from the introduction

but no disjunct is entailed without UNA. To show the second claim observe that T2,A |=UNA q(⃗a) iff ∅,A′ |= q(⃗a) holds for every ABox A, any CQ q, and for A′ obtained from A by adding the assertions ProlificAuthor(b) for any b such that author(b, c) ∈ A for at least 200 distinct c. It follows immediately that T2 has the ELIQ=-disjunction property with UNA and enjoys PTIME CQ-evaluation with UNA.

We need the following technical lemma.

Lemma 1. If T is an ALCHIQ TBox, then T has the ELIQdisjunction property iff T has the ELIQ=-disjunction property iff T has the CQ-disjunction property. The equivalences hold both with and without UNA.

Proof (sketch). We prove the case without UNA of which the case with UNA is a special case. The direction from CQ to ELIQ is trivial. For the direction from ELIQ to ELIQ=, we simulate equalities between distinct individual names in an ABox A by ELIQs as follows. Given an equality (a = b) with a ̸= b ∈ ind(A), we first extend A by a new assertion Aa(a), where Aa is a fresh concept name, and then replace (a = b) by Aa(b). Note that the corresponding query Aa(x) is an ELIQ. The direction from ELIQ= to CQ is similar to the proof of Theorem 16 in [Lutz and Wolter, 2017].

For an ABox A and an equivalence relation ∼ on ind(A), the quotient ABox A/∼ of A is defined by replacing each individual a in A with the equivalence class a/∼ of a w.r.t. ∼. Given a tuple ⃗a = (a1, . . . , ak) in A we denote by ⃗a/∼ the tuple (a1/∼, . . . , ak/∼).

Theorem 1. A Horn-ALCHIQ TBox T ′ is a CQ-Horn-rewriting of an ALCHIQ TBox T without UNA iff it is a CQHorn-rewriting of T with UNA.

Proof (sketch). For the direction from left to right, let A be an ABox. We first establish that for all CQs q1(⃗x1), . . . , qn(⃗xn) and tuples ⃗a1, . . . ,⃗an in A:

For the proof, we may assume that the qi(⃗xi) are ELIQs (by Lemma 1). We then simulate disjunctions of ELIQs by single ELIQs (see Theorem 18 in [Lutz and Wolter, 2017] for a similar construction) and use that T ′ is a CQ-Horn-rewriting of T without UNA.

Now let q(⃗x) be a CQ and ⃗a a tuple in A. Then, (1) and (2) imply T ,A |=UNA q(⃗a) iff T ′ ,A |=UNA q(⃗a).

For the converse, we first establish that T ,A |=nUNA q(⃗a) iff T ,A/∼ |=UNA q(⃗a/∼) for all equivalence relations ∼ on ind(A), where A, q(⃗x), and ⃗a are as above. The same holds if we substitute T ′ for T . Since the right hand side of this equivalence holds for T iff it holds for T ′ , it follows that T ,A |=nUNA q(⃗a) iff T ′ ,A |=nUNA q(⃗a).

We now turn to CQ-evaluation w.r.t. ALCHIQ TBoxes. As shown in [Hernich et al., 2017], the ELIQ=-disjunction property implies that CQ-evaluation with UNA is in PTIME. The proof can be generalized to the case without UNA.

Lemma 2. Let T be a ALCHIQ TBox. If T does not have the ELIQ=-disjunction property, then ELIQ=-evaluation for T is CONP-hard. This holds both with and without UNA.

Example 2. As the TBox T2 from Example 1 does not enjoy the ELIQ=-disjunction property without UNA, CQ-evaluation w.r.t. T2 is CONP-hard without UNA.

As a consequence of Lemma 2 we obtain that tractability of CQ-evaluation without UNA implies tractability of CQevaluation with UNA.

Theorem 2. Let T be an ALCHIQ TBox and suppose that CQ-evaluation w.r.t. T without UNA is in PTIME. Then, CQevaluation w.r.t. T with UNA is in PTIME.

Proof. We reduce the UNA case to the non-UNA case. Let A be an ABox, q(⃗x) a CQ, and ⃗a a tuple in A. By Lemma 2 and Lemma 1, T has the CQ-disjunction property (unless we are in the trivial case where PTIME = CONP). Now, (1) implies that T ,A |=UNA q(⃗a) iff either T ,A |=nUNA q(⃗a) or there exist a ̸= b ∈ ind(A) with T , A |=nUNA (a = b).

4 CQ-Horn-Rewritability vs PTIME w/o UNA

We show that, without the UNA, CQ-Horn-rewritability captures PTIME query evaluation for ALCHIQ TBoxes of depth 1. We also show that the meta problem of deciding CQ-Horn-rewritability is EXPTIME complete for such TBoxes. To prove these results, we first show how to equivalently transform a TBox of depth 1 into a certain normal form. From the resulting TBox T we construct a Horn TBox Thorn which we show to be a CQ-Horn-rewriting of T if and only if CQevaluation for T is in PTIME.

We start with the normal form. A literal is a concept name or a negation thereof. A CI C ⊑ D is in normal form if

1. C is a conjunction of concept names and concepts of the form (⩾ n r E) with E a conjunction of concept names;
2. D is a disjunction of
3. concept names;
4. concepts (⩾ n r E) with E a conjunction of literals;
5. concepts (⩽ n r E) with E a conjunction of literals that contains at least one negative literal.

We set C = ⊤ if C is the empty conjunction and D = ⊥ := ¬⊤ if D is the empty disjunction. An ALCHIQ TBox T is in normal form if all CIs in T are in normal form.

Lemma 3. Every ALCHIQ TBox T of depth 1 can be converted into a logically equivalent ALCHIQ TBox T ′ in normal form.

In the worst case, T ′ is of size double exponential in the size T . From now on, we assume that T is fixed and in normal form. Using T , we define a Horn TBox Thorn. For any conjunction or disjunction of literals E, we use pos(E) to denote the conjunction of all concept names A in E and neg(E) to denote the conjunction of all concept names A such that ¬A is in E. We use LT to denote the set of

• concept names or concepts of the form (⩾ nrE) occurring as top-level conjuncts in C in some CI C ⊑ D ∈ T ;
• concepts (⩾ n + 1 r pos(E)) such that there is a CI C ⊑ D ∈ T such that (⩽ n r E) is a disjunct of D.

A set S ⊆ LT is a trigger for a CI C ⊑ D ∈ T if S contains all top-level conjuncts of C and all (⩾ n+1 r pos(E)) with (⩽ n r E) a disjunct of D. For a trigger S, we denote by CS the conjunction of all concepts in S and by C ≤1 S the ELI concept obtained from CS by replacing every (⩾ n r E) with n ≥ 2 by (⩾ 1 r E). For a concept (⩽ n r E) with E a conjunction of literals that contains at least one negative literal, we call ∀r.E′ a Horn specialization of (⩽ n r E) if E′ is obtained from E by dropping all but one negative literal. We sometimes write Horn specializations in the form ∀r.(A1 ⊓ · · · ⊓ An → A) where C → D stands for ¬C ⊔ D.

For each CI C ⊑ D ∈ T and trigger S for it we define a set Horn(C ⊑ D, S) of Horn-ALCIQ-CIs. In the special case that T |= C ≤1 S ⊑ ⊥we set Horn(C ⊑D, S) = {C ≤1 S ⊑ ⊥}. Otherwise Horn(C ⊑ D, S) contains the following CIs whenever they are a consequence of T :

• C ≤1 S ⊑ (⩽ 1 rE) if (⩾ nrE) ∈ S for some n ≥ 2;
• C ≤1 S ⊑ A if A ∈ NC is a top-level disjunct of D;
• C ≤1 S ⊑ R if R = ∀r.(A1 ⊓ · · · ⊓ An → A) is a Horn specialization of some disjunct (⩽ n r E) of D;
• C ≤1 S ⊑ (⩾ 1 r pos(E)) if (⩾ mrE) is a disjunct of D such that T ̸|= C ≤1 S ⊑ ¬(⩾mrE).

Now the Horn-ALCHIQ TBox Thorn is defined as the union of all RIs in T and

It can be verified that, by construction, T |= Thorn. The following lemma is the main step towards the capturing result.

Lemma 4. Let T be an ALCHIQ TBox in normal form. Then the following conditions are equivalent:

1. T has the ELIQ=-disjunction property without UNA;
2. for every C ⊑ D ∈ T and trigger S for C ⊑ D, Horn(C ⊑ D, S) ̸= ∅;
3. T and Thorn are CQ-inseparable without UNA.

The following examples illustrate this lemma.

Example 3. (1) Reconsider the TBox T1 from the introduction, which contains the only CI

∃author.Short Story ⊔ ∃author.¬Fiction

that we abbreviate by α. Then S = {∃author.⊤} is the only trigger for α. We have T1horn = Horn(α, S) = {∃author.⊤ ⊑ ∃author.⊤} since pos(¬Fiction) = ⊤. Thus, Horn(α, S) ̸= ∅ and, by Lemma 4, T1horn is a CQ-Horn-rewriting of T1 (equivalent to the empty TBox) .

Define T ′ by adding to T1 the CI Novelist ⊑ ∀author.Fiction. Then S = {∃author.⊤,Novelist} is a trigger for α and now Horn(α, S) = ∅. Thus, by Point 2, T ′ horn is not a CQ-Horn-rewriting of T ′ .

(2) Consider the TBox T2 from the introduction containing

Then S = {(⩾ 200 author ⊤)} is the only trigger for β. We have C ≤1 S = ∃author.⊤ and it is readily checked that T2horn = Horn(β, S) = ∅. By Point 2, T2horn is not a CQ-Horn-rewriting of T2.

(3) Observe that for any TBox T , 0, 1 are the only numbers used in Thorn. Consider, for example, T = {ProlificScientist ⊑ (⩾ 200author ¬Fiction)}. Then Thorn = {ProlificScientist ⊑ (⩾ 1 author ⊤)} is a CQ-Hornrewriting of T .

We give a brief description of the proof of Lemma 4. For the proof of (1) ⇒ (2) one constructs under the assumption that (2) does not hold for C ⊑ D and trigger S the tree-shaped ABox AS corresponding to the concept CS and a disjunction of queries in ELIQ= which refutes the ELIQ=-disjunction property if Horn(C ⊑ D, S) = ∅. For (2) ⇒ (3) one defines a chase procedure which constructs, if (2) holds, for every ABox A satisfiable w.r.t. Thorn a universal model of A and Thorn which is also a model of T . For (3) ⇒ (1) assume that (3) holds and let A be an ABox, q1(⃗x1), . . . , qn(⃗xn) CQs, and ⃗a1, . . . ,⃗an tuples in A with T , A |=nUNA∨1≤i≤nqi(⃗ai). By (2) from the proof of Theorem 1, Thorn,A |=nUNA∨1≤i≤nqi(⃗ai). But then there exists i such that Thorn,A |=nUNAqi(⃗ai) and by Point 3, T ,A |=nUNAqi(⃗ai), as required.

The following main result of this section now follows from Lemmas 4 and 2.

Theorem 3. CQ-Horn-rewritability captures PTIME CQevaluation without UNA for ALCHIQ TBoxes of depth 1 (unless PTIME equals CONP).

Observe that we also obtain a PTIME/CONP dichotomy for CQ-evaluation w.r.t. ALCHIQ TBoxes of depth 1, without the UNA: for any such TBox T , CQ-evaluation is in PTIME for all CQs or there exists a CQ for which query evaluation is CONP-hard w.r.t. T . Results of this form have so far only been obtained for query evaluation with UNA [Lutz and Wolter, 2017; Hernich et al., 2017].

Point 2 of Lemma 4 provides an effective algorithm for checking CQ-Horn-rewritability. Note, however, that because of the double exponential blow-up in the normalization step for TBoxes and the potentially exponential number of triggers, its worst-case complexity is triple exponential. Using a modeltheoretic approach, we improve this to a single-exponential upper bound, and thus deciding CQ-Horn-rewritability is not harder than satisfiability.

Theorem 4. Deciding CQ-Horn-rewritability of ALCHIQ TBoxes of depth 1 is EXPTIME-complete.

The lower bound is proved by a polynomial reduction of the satisfiability of ALCHIQ TBoxes. For the upper bound, one decides the ELIQ=-disjunction property without UNA. Using a model-theoretic reformulation one can show that a TBox T has the ELIQ=-disjunction property without UNA iff it has the Q-disjunction property without UNA for ABoxes that have the shape of a tree of depth 1 and of outdegree bounded by |T |, where Q is the class of ELIQ=s of depth 1 and of outdegree bounded by |T |, and where both the ABox and the queries use concept and role names from T only. The latter condition can be reduced to satisfiability in ALCHIQ.

5 CQ-Horn-Rewritability vs PTIME with UNA

As shown in Examples 1 and 2, CQ-Horn-rewritability does not capture PTIME query evaluation with UNA for very simple ALCQ-TBoxes of depth 1 (unless PTIME equals CONP). The experiments reported in the introduction further show that the CIs occurring in these TBoxes are very common in practice. The following example shows that when number restrictions are restricted to global functionality assertions, then there are still TBoxes of depth 1 for which CQ-evaluation is in PTIME with UNA but which are not CQ-Horn-rewritable.

Example 4. Let T be the ALCHIF TBox stating that role names s1 and s2 are functional and containing the RIs r ⊑ s1 and r ⊑ s2 and the CIs

One can show that T has the CQ-disjunction property with UNA but not without UNA. Thus, CQ-evaluation w.r.t. T with UNA is in PTIME [Hernich et al., 2017] and T is not CQ-Horn-rewritable. To refute the CQ-disjunction property without UNA, let A = {s1(a, b1), s2(a, b2)}. Then T , A |=nUNA B(a) ∨∃r.⊤(a) but T , A ̸|=nUNA B(a) since by identifying b1 and b2 and adding (a, bi) to the extension of r and bi to B1 and B2 one can define a model I of T and A such that aI ̸∈ BI ; and T ,A ̸|=nUNA ∃r.⊤(a) since by adding a to the extension of B, b1 to B1, and b2 to B2 one can define a model I of T and A such that aI ̸∈ (∃r.⊤)I . To show the CQ-disjunction property with UNA, one can construct for any ABox A satisfiable w.r.t. T with UNA a model I which maps homomorphically into any model of A and T with UNA.

We now show that the interaction between functionality assertions and RIs exploited in Example 4 is needed to construct TBoxes in ALCHIF which are not CQ-Horn-rewritable but for which CQ-evaluation is in PTIME with UNA. An ALCHIF ⊑f TBox is an ALCHIF TBox T such that whenever r ⊑ s ∈ T , then neither s nor s- are functional in T .

Theorem 5. Let T be an ALCHIF ⊑f TBox. Then CQevaluation w.r.t. T without UNA is in PTIME iff CQ-evaluation w.r.t. T with UNA is in PTIME.

Proof (sketch). The direction (⇒) is Theorem 2. Conversely, assume that CQ-evaluation with UNA is in PTIME. Let A be an ABox. Let ∼ be the smallest equivalence relation on ind(A) such that if a ∼ b and r(a, a′ ), r(b, b′ ) ∈ A and ⊤ ⊑ (⩽ 1 r ⊤) ∈ T , then a′ ∼ b′ . One can show that T , A |=nUNA q(⃗a) iff T ,A/∼ |=UNA q(⃗a/∼), for every CQ q and tuple ⃗a in ind(A). It follows that CQ-evaluation without UNA is in PTIME since ∼ can be computed in polynomial time.

The following is now a consequence of Theorems 5 and 3.

Theorem 6. CQ-Horn-rewritability captures PTIME query evaluation with UNA for all ALCHIF ⊑f TBoxes of depth 1 (unless PTIME equals CONP).

So far, we have investigated the relationship between PTIME CQ-evaluation and CQ-Horn-rewritability mainly for TBoxes of depth 1. In fact, our results for depth 1 TBoxes do not generalize to arbitrary depth.

Theorem 7. CQ-Horn-rewritability does not capture PTIME query evaluation for ALC TBoxes of depth 3 (with and without UNA).

Proof. According to Theorem 6.8 in [Lutz and Wolter, 2017] there are ALC TBoxes T of depth 3 such that CQ-evaluation w.r.t. T is in PTIME but such that some CQs q are not Datalog-rewritable w.r.t. T . Such a TBox cannot be CQ-Hornrewritable since every CQ is Datalog-rewritable w.r.t. any Horn-ALC TBox [Lutz and Wolter, 2017].

The question whether CQ-Horn-rewritability captures PTIME query evaluation for ALC TBoxes of depth 2 is open. Decidability of CQ-Horn-rewritability for ALC TBoxes of arbitrary depth is also open. For ALCF, however, one can easily extend Theorem 7.3 in [Lutz and Wolter, 2017] and show that CQ-Horn-rewritability of ALCF TBoxes of depth 3 is undecidable.

6 Discussion

We briefly discuss alternative approaches to rewritability into Horn TBoxes. From a logical viewpoint, it is natural to demand that the rewriting T ′ should not only give the same answers to CQs as T , but be logically equivalent to T , or at least a conservative extension. Here, T ′ is called a conservative extension of T if T ′ |= α for every α ∈ T and for every model of T there exists a model of T ′ which coincides with T regarding its domain and the interpretation of the concept and role names from T . Unfortunately, this approach is extremely restrictive. We have seen that the TBox T1 from the introduction is trivial from the viewpoint of answering CQs (it is CQ-inseparable from the empty TBox), but nevertheless there is no conservative extension of T1 which is also a Horn TBox. One can show this by proving that no conservative extension of T1 is preserved under direct products.

In some applications of ontology-mediated querying the user knows in advance signatures (finite sets of concept and role names) Σ1 and Σ2 such that all relevant ABoxes and CQs use symbols fromΣ1 and, respectively, Σ2 only. Then, rather than admitting arbitrary ABoxes and CQs in the definition of CQ-Horn-rewritings, it is natural to consider CQ-Hornrewritings w.r.t (Σ1,Σ2) in the sense that T and T ′ give exactly the same answers to all CQs in Σ1 on all ABoxes in Σ2. The corresponding notion of (Σ1, Σ2)-inseparability has been considered in [Botoeva et al., 2016b]. This relaxation leads to undecidability of CQ-Horn-rewritability as one can reduce the corresponding undecidable CQ-inseparability problem.

Theorem 8. For ALC TBoxes of depth 1 there is no algorithm that decides CQ-Horn-rewritability w.r.t. (Σ1, Σ2) and outputs such a rewriting in case it exists.

7 Conclusion

We have investigated whether CQ-Horn-rewritability captures PTIME query evaluation, with particular focus on the influence of the UNA and the depth of TBoxes. From a practical viewpoint it would be of interest to investigate query answering algorithms covering the CIs which are in PTIME but cannot be captured using Horn-CIs discussed in the introduction. It would also be of interest to investigate the succinctness of CQ-Horn-rewritings. The normal form of a given TBox is of double exponential size (in the worst case) and our CQinseparable rewritings are of exponential size in the size of the TBox in normal form. It is open whether this is optimal.

Acknowledgements

Andr´e Hernich, Fabio Papacchini, and Frank Wolter were supported by EPSRC UK grant EP/M012646/1 and Carsten Lutz was supported by the DFG-funded Collaborative Research Center EASE.