Making Cross Products and Guarded Ontology Languages Compatible

1 Introduction

Ontology-based data access (OBDA) has recently emerged as a promising application of AI technologies in information management systems [Poggi et al., 2008]. Actually, OBDA refers to the utilization of ontologies for providing a unified conceptual view of various data sources. Users can then pose their queries solely in the schema provided by the ontology, abstracting away from the specifics of the sources. In this setting, the actual user query and the ontology can be interpreted as two components of one composite query, called ontologymediated query (OMQ) [Bienvenu et al., 2014]. Thus, OBDA is often realized as the problem of answering OMQs.

In the OMQ setting, the ontology is a set of first-order sentences, while the query is a union of conjunctive queries. Of course, in its full generality, the problem of evaluating OMQs is very hard (in fact, undecidable) due to the very high expressiveness of first-order logic. This gave rise to a flourishing research activity in the KR community towards the discovery of ontology languages that achieve the right balance between expressivity and complexity. Consequently, a significant range of ontology languages, which vary in syntax, expressivity and complexity, has been developed. Two prominent families of languages, obtained from this extensive effort, are description logics (DLs) and existential rules (a.k.a. Datalog± rules).

Many of the existing DL-based and rule-based ontology languages guarantee good computational and model-theoretic properties by implicitly posing some restrictions on the use of quantifiers. They are essentially defined through the relativisation of quantifiers by atomic formulas, an idea that goes back to the guarded fragment of first-order logic, introduced with the aim of explaining and generalizing the good properties of modal logic [Andr´eka et al., 1998]. In fact, the guarded fragment serves as a unifying framework that subsumes many DL-based and rule-based ontology languages.

Although guardedness is a well-established paradigm that gives rise to highly expressive and robust ontology languages, the relativised nature of the permitted quantifiers excludes key modeling features that are very useful for knowledge representation purposes. Prominent examples of such features are transitivity and cross products. The former allows us to state that a binary relation is transitive; for example,

states that the descendant relation is transitive. The latter allows us to define relations that connect every instance in a relation with every instance in another relation; for example,

states that elephants are bigger than mice by defining the binary relation BiggerThan that connects every instance in the class Elephant with every instance in the class Mouse.

The question whether the feature of transitivity is compatible with the guarded fragment, or with DL/rule-based subfragments of it, has attracted considerable attention in the logic and KR communities; see, e.g., [Ganzinger et al., 1999; Szwast and Tendera, 2004; Eiter et al., 2009; Gottlob et al., 2013; Baget et al., 2015; Amarilli et al., 2016] (let us stress that the list is by no means exhaustive). On the other hand, the same question for cross products has received far less attention. To the best of our knowledge, the only work that explicitly studies this question is [Rudolph et al., 2008], where the concept product is investigated as an expressive feature for DLs. The above cross product is actually a concept product, which, in DL syntax, is written as

Elephant × Mouse ⊑ BiggerThan.1

The main message of [Rudolph et al., 2008] is that concept products are, in general, compatible with DLs. Notice that the above work focuses on the problem of satisfiability, that is, given an ontology, to decide whether it has at least one model. However, by exploiting techniques developed in [Rudolph et al., 2008], one can easily show that expressive DLs are compatible with concept products even for OMQ evaluation purposes. To sum up, we know that satisfiability for the highly expressive DL SROIQ extended with concept products is decidable, and OMQ evaluation for ALCHOI extended with concept products is also decidable.

The goal of this work is to answer the question whether cross products are compatible with existing guarded-based ontology languages that deviate from DLs, both for satisfiability and OMQ evaluation purposes. To this end, we focus on the guarded fragment of first-order logic, which, as said above, serves as a unifying framework that subsumes many of the existing ontology languages that rely on guardedness, and we investigate the reasoning tasks of satisfiability and OMQ evaluation. Our contributions can be summarized as follows:

• ◮ After extending the guarded fragment with cross products, we focus on satisfiability. The decidability of the problem depends on the arity of the cross products, i.e., the arity of the relation defined by the cross product; e.g., the above cross product is binary. We show that the problem is undecidable, even for ternary cross products, but 2EXPTIME-complete for binary cross products. Hence, the decidability/undecidability frontier lies between ternary and binary cross products.
• ◮ We then turn our attention to OMQ evaluation, and we show that the situation changes dramatically. The problem is undecidable, even if we focus on the two-variable fragment of the guarded fragment extended with binary cross products. Our main finding here is that, for OMQ evaluation purposes, cross products are not compatible with the guarded fragment.
• ◮ Given the negative result above, we investigate whether by restricting the query or the ontology language we can obtain decidability. We first restrict the query language and focus on acyclic UCQs. In this case, OMQ evaluation under the (full) guarded fragment extended with binary cross products is 2EXPTIME-complete in the combined, and coNP-complete in the data complexity. We then focus on arbitrary UCQs, and show that OMQ evaluation under guarded existential rules with binary cross products is 2EXPTIME-complete in the combined, and PTIME-complete in the data complexity; the latter holds even for frontier-guarded existential rules, which are incomparable to the guarded fragment. The above results show that, in some relevant cases, binary cross products can be considered without paying a price in terms of complexity.

2 Preliminaries

Interpretations and Queries. Let C, N, and V be pairwise disjoint countably infinite sets of constants, (labeled) nulls and (regular) variables, respectively. Different constants represent different values (unique name assumption), while different nulls may represent the same value. A schema S is a finite set of relation symbols with associated arity; we write R/n to denote that R has arity n. A term is either a constant, null or variable. An atom over S is an expression R(¯ t), where R/n ∈ S and ¯ t is an n-tuple of terms. An interpretation over S is a (possibly infinite) set of atoms over S that contains only constants and nulls, while a database over S is a finite interpretation over S that contains only constants. We may call an interpretation and a database over S an S-interpretation and S-database, respectively. The domain of an interpretation I, denoted dom(I), is the set of all terms occurring in I.

1 This is actually the title of [Rudolph et al., 2008], i.e., "All Elphants are Bigger than All Mice".

A conjunctive query (CQ) over S is a formula of the form q(¯x) = ∃¯ y(R1(¯ v1) ∧ · · · ∧ Rm(¯ vm)), where each Ri(¯ vi) (1 ≤ i ≤ m) is an atom without nulls over S, each variable mentioned in the ¯ vi's appears either in ¯ x or ¯ y, and ¯x are the free variables of q. If ¯x is empty, then q is a Boolean CQ. As usual, the evaluation of CQs is defined in terms of homomorphisms. Let I be an instance and q(¯x) a CQ as above. A homomorphism from q to I is a mapping h, which is the identity on C, from the variables that appear in q to dom(I) such that Ri(h(¯ vi)) ∈ I, for each 1 ≤ i ≤ m. The evaluation of q(¯x) over I, denoted q(I), is the set of all tuples h(¯x) of constants such that h is a homomorphism from q to I. We denote by CQ the class of conjunctive queries. A union of conjunctive queries (UCQ) over S is a formula of the form q(¯x) := q1(¯x) ∨ · · · ∨ qn(¯x), where each qi(¯x) is a CQ. The evaluation of q(¯x) over I, denoted q(I), is the set of tuples ∪1≤i≤nqi(I). We denote by UCQ the class of UCQs.

Ontologies. An ontology language L is a (possibly infinite) set of first-order sentences that can mention constants and variables-nulls and function symbols are not allowed. An ontology Σ that falls in L, or simply L-ontology, is a finite set of sentences from L. Concrete ontology languages, which are based on the guarded fragment, are discussed in the next section. An interpretation I is a model of an ontology Σ, written I |= Σ, if it satisfies all its sentences, and it is a model of a database D, written I |= D, if D ⊆ I.

Ontology-Mediated Queries. An ontology-mediated query (OMQ) is a pair Q = (Σ, q(¯x)), where Σ is an ontology and q a UCQ. Given a database D, the evaluation of Q over D is defined as ∩I|=D,I|=Σ {¯ c ∈ dom(D)|¯x| | ¯ c ∈ q(I)}, i.e., the certain answers to q w.r.t. D and Σ, and is denoted Q(D). We write (L,CQ) for the OMQ language that consists of all OMQs of the form (Σ, q), where Σ is an L-ontology and q ∈ CQ. The language (L, UCQ) is defined analogously.

Reasoning Tasks. We concentrate on the two main reasoning tasks that involve ontologies and OMQs, that is, satisfiability and query evaluation, respectively. Satisfiability simply asks whether a given ontology admits at least one model:

PROBLEM : Sat(L)

INPUT :

An L-ontology Σ.

QUESTION : Does Σ has at least one model?

As is customary when studying the complexity of the evaluation problem for a query language, we consider its associated decision problem, i.e., whether a tuple of constants belongs to the evaluation of a query over a database:

PROBLEM : Eval(L,Q)

INPUT :

An OMQ Q = (Σ, q(¯x)) ∈ (L, Q),

a database D, and ¯ c ∈ dom(D)|¯x| .

QUESTION : Does ¯

c ∈ Q(D)?

For the evaluation problem, we focus on the standard complexity measures: combined complexity, calculated by considering both the database and the query as part of the input, and data complexity, where the query is fixed.

3 Guarded Fragment with Cross Products

The primary goal of this work is to perform an in-depth complexity analysis of the above crucial tasks in the presence of ontologies that fall in an extended version of the guarded fragment that allows cross products. Let us first recall the guarded fragment, and then extend it with cross products.

Guarded Fragment. The guarded fragment of first-order logic, introduced in [Andr´eka et al., 1998], is a collection of first-order formulas with some syntactic restrictions on quantification patterns. We write GF for the smallest set of formulas (over a schema S) that (i) contains all atoms over S; 2 (ii) is closed under ¬, ∧, ∨, →; and (iii) if α is an atom containing all the variables of (¯x ∪ ¯ y), and ϕ ∈ GF with free variables in (¯x ∪ ¯ y), then ∀¯x(α → ϕ) and ∃¯x(α ∧ ϕ) belong to GF as well; the atom α is called the guard of the quantifier. Sat(GF) has been studied in [Gr¨adel, 1999], and Eval(GF, UCQ) in [B´ar´any et al., 2014]: 3

Proposition 1 The following holds:

1. Sat(GF) is 2EXPTIME-complete.
2. Eval(GF,UCQ) is 2EXPTIME-complete in the combined, and coNP-complete in the data complexity.

Adding Cross Products. We proceed to extend the guarded fragment with cross products. Let us first make the notion of cross product more precise. A k-ary cross product over a schema S, where k ≥ 2, is a first-order formula ϕ of the form

where the following conditions hold: R/n, S/m and T/k belong to S, xi ̸= xj (1 ≤ i < j ≤ n), yi ̸= yj (1 ≤ i < j ≤ m), {x1, . . . , xn}∩{y1, . . . , ym} = ∅, 1 ≤ i1 < · · · < iℓ ≤ n, and 1 ≤ j1 < · · · < jp ≤ m. Let us clarify that the arity of ϕ is the arity of the relation T that appears in the righthand side of "→". Moreover, n, m > 0, i.e., the relations that appear in the left-hand side of "→" are at least unary; hence, the arity of a cross product is at least two. We call ϕ full if x1, . . . , xn = xi1 , . . . , xiℓ and y1, . . . , ym = yj1 , . . . , xjp , i.e., a full cross product computes the cross product of two relations without projecting any of their positions.

2 For technical clarity we exclude equalities; however, our results hold even for the guarded fragment with equalities.

3 The work [B´ar´any et al., 2014] does not explicitly consider OMQs, but its results can be effortlessly transferred to OMQs.

Example 1 Given two relations R/3 and S/2, we can compute their cross product via the full 5-ary cross product

Now, if we need their partial cross product focussing, e.g., on the first and third position of R, and the second position of S, we can use the (partial) ternary cross product

which first applies a projection operator, and then computes the cross product of the projected positions.

Let CPk be the set of all i-ary cross products, where 2 ≤ i ≤ k. We define CP as the set ∪k≥2CPk , that is, the set of all cross products. The guarded fragment with cross products is defined as the set of first-order formulas GF× = GF∪CP. We also write GF×k , where k ≥ 2, for the set GF ∪ CPk .

Partial vs. Full Cross Products. At this point, one may be tempted to think that partial cross products are more powerful than full cross products since the former can compute the cross product of some projected positions of the involved relations. This is not true since the projection can be simulated using guarded formulas. In the sequel, we assume, w.l.o.g., that GF×-ontologies contain only full cross products.

4 Satisfiability of GF×

Having the formal definition of GF× in place, we are now ready to proceed with our reasoning tasks. In this section, we focus on Sat(GF×). Although Sat(GF) is decidable [Gr¨adel, 1999], Sat(GF×) is undecidable, even for ternary cross products. The reason for this negative result is because with GF×3 we can state that a binary relation is transitive. However, if we focus on binary cross products, then the problem in question is decidable, and, in particular, 2EXPTIME-complete. Therefore, we can safely conclude that the frontier between decidability and undecidality of Sat(GF×) lies between GF×2 and GF×3 . In the rest of this section we discuss the above results.

4.1 Ternary Cross Products

We start by showing the following negative result:

The key observation underlying the proof of the above result is that the transitivity axiom

which states that the relation R is transitive, can be simulated by a set of formulas that fall in GF×3 . This fact allows us to reduce the satisfiability problem for the guarded fragment with transitivity (GFtr ), which is an undecidable problem [Ganzinger et al., 1999; Gr¨adel, 1999], to Sat(GF×3 ).

Consider a GFtr -ontology Σ over a schema S. Let Σ′ be the ontology over S′ ⊇ S obtained from Σ by replacing each transitivity axiom that has the form of ϕtr above with

where R1 and TR do not belong to S. It is easy to show that Σ and Σ′ are equisatisfiable. Moreover, although {ψ1, ψ2, ψ3} does not directly fall in GF×3 , it can be equivalently rewritten as a set of formulas that fall in GF×3 , and Theorem 2 follows.

Cross Product Guards. Sat(GFtr ) becomes decidable if we focus on transitive guards, i.e., the transitive relations appear only in guards [Ganzinger et al., 1999; Szwast and Tendera, 2004]. Hence, one may be tempted to think that by focussing on cross product guards, i.e., forcing the relations that appear in the right-hand side of a cross product to appear only in guards, we ensure the decidability of Sat(GF×3 ). This is not the case since the construction underlying Theorem 2 does not use a cross product relation outside a guard.

4.2 Binary Cross Products

Theorem 2 confirms that even ternary cross products are not compatible with GF. However, binary cross products can be simulated by guarded formulas, which allows us to show that:

The lower bound is inherited from Proposition 1. We now discuss the main ingredients of the reduction to Sat(GF).

Normalization and the Chase. A GF×2 -ontology Σ can be rewritten in polynomial time into an ontology Σ′ that contains only one binary cross product of the form

and each sentence of Σ′ \ {ϕcp} is either of the form

where ϕ, ψi are conjunctions of atoms, and ϕ has an atom that contains all the variables (¯x ∪ ¯ y), or

where ϕ has an atom that contains all the variables ¯x, and ⊥ denotes false. Sentences of the form (1) are known as guarded disjunctive existential rules (or guarded disjunctive tuple-generating dependencies), while sentences of the form (2) are known as guarded negative constraints. Although sentences of the form (1) and (2) do not directly fall in GF, they can be transformed in linear time into GF sentences.

The crucial property of normalized ontologies Σ is that for satisfiability purposes it suffices to focus on a canonical set of models, which acts as a representative of all the other models of Σ. It can be constructed via the disjunctive chase, a natural generalization of the well-known chase procedure for existential rules. We assume the reader is familiar with the disjunctive chase; for details, see, e.g., [Bourhis et al., 2016]. We write dchase(Σ) for the set of models of Σ constructed by the disjunctive chase-we know that Σ is satisfiable iff there exists I ∈ dchase(Σ) that satisfies all the negative constraints occurring in Σ. Moreover, we can refer to the subtree of an atom in a chase interpretation, a useful notion that we heavily exploit in our analysis. Consider an interpretation I ∈ dchase(Σ). Roughly speaking, the subtree of an atom α ∈ I, denoted Tα, is inductively defined as follows: (i) α is the root of Tα, and (ii) if an atom β is obtained from the atoms β1, . . . , βn by applying a guarded rule ϕ, where the witness βi of the guard atom of ϕ belongs to Tα, then there exists an edge from βi to β. In what follows, we fix an ontology Σ over a schema S obtained after normalizing a GF×2 ontology.

Harmless Applications of the Cross Product. The goal is to translate Σ into an equisatisfiable GF-ontology by simulating the applications of the cross product ϕcp, during the disjunctive chase, via guarded formulas. Interestingly, some of those applications are harmless, and they can easily be simulated via guarded rules. Assume that the atom α = Cross(t1, t2) is obtained by applying ϕcp. Such an application of the cross product is harmless if the atoms Term(t1) and Term(t2), due to which ϕcp has been applied, have a common ancestor β that contains both t1 and t2. In this case, we can convert ϕcp into a guarded rule via a guard atom G(x, y) that can be computed from β. We simply need to add to Σ the rules:

From the above discussion, we can safely assume that whenever the cross product ϕcp is being applied due to Term(t1) and Term(t2), the latter atoms do not have a common ancestor that contains both t1 and t2. These are the applications of ϕcp that we call dangerous, which we discuss below.

Dangerous Applications of the Cross Product. The dangerous applications of ϕcp are responsible for the violation of the key model-theoretic property of the chase under guarded rules, which, for brevity, we call guarded property. Roughly, the guarded property states that if we focus on a certain interpretation I ∈ dchase(Σ), the atoms that are involved in the application of a guarded rule ϕ during the construction of I, have a common ancestor in I, or, in other words, they are connected in I. This property does not hold in the presence of the cross product since a situation like the one illustrated in Figure 1 may occur. Assuming that α = Cross(t1, t2), it is possible that an atom γ generated inside Tα acts as the witness of a non-guard atom during the application of a guarded rule ϕ, and the atom δ that belongs to Tβ is generated. Notice that Tα and Tβ are disjoint trees since the atoms of the form Cross(·, ·), obtained via the cross product, give rise to new trees that are disconnected with the rest of I. Let us examine more carefully the reason that causes this situation.

Recall that the atoms Term(t1) and Term(t2) do not have a common ancestor that contains both t1 and t2. At the same time, it may be the case that Term(ti), for i ∈ {1, 2}, and β have a common ancestor; thus, β may contain the term ti. Consequently, the atom γ, which belongs to Tα, may be involved in the application of the guarded rule ϕ that generates δ, which belongs to Tβ; hence, the guarded property is violated since Tα and Tβ are disjoint trees. The key observation, however, is that γ contains only the term ti. Intuitively, this means that the only atoms of Tα that can affect some other disjoint tree Tβ, or, they are "visible" from Tβ, are atoms of the form P(t, . . . , t), where t ∈ {t1, t2}. This is the crucial observation that allows us to simulate the dangerous applications of ϕcp via guarded formulas.

Terms and Types. The above observation led us to introduce the notion of the type for a term in an interpretation. Given an interpretation I over a schema S and a term t ∈ dom(I), the type of t in I is defined as the set of relations

We call I ∈ dchase(Σ) type invariant if the following holds: for each α = Cross(t1, t2) ∈ I and β = Cross(t3, t4) ∈ I such that typeI(t1) = typeI(t3) and typeI(t2) = typeI(t4), Tα and Tβ are isomorphic. Interestingly, if Σ is satisfiable, then there exists a type invariant I ∈ dchase(Σ) that satisfies all the guarded negative constraints of Σ. 4 This fact, together with the observation that the atoms inside a tree TCross(t,t′ ) that are visible from other disjoint trees depend solely on the types of t and t′ , brings us to the main idea underlying the transformation of Σ into an equisatisfiable GF-ontology. The intention is to simulate a type invariant I ∈ dchase(Σ) by generating, via GF formulas, trees that act as representatives of the isomorphic trees in I rooted at Cross(·, ·) atoms.

Transformation of Σ into a GF-ontology. We make use of the following auxiliary relations (in the sequel, T ∈ 2S ): (i) PartialT (t) means that T is a subset of the type of the term t in some chase interpretation, (ii) FullT (t) means that T is the actual type of t in some chase interpretation, and (iii) [T1, T2, T3, T4](t1, t2), where T1, . . . , T4 ∈ 2S, T1 ⊆ T2 and T3 ⊆ T4, means that the partial type of t1 and t2 constructed so far is T1 and T3, respectively, while T2 and T4 is the actual type of t1 and t2, respectively, that eventually should be constructed. The atoms in (iii) are auxiliary atoms that are used to inductively generate the atom [T, T, T ′, T ′ ](t1, t2), which acts as the representative for the atoms Cross(t, t′ ) occurring in a chase interpretation I such that typeI (t) = T and typeI (t′ ) = T ′ . We obtain Σ+ by adding to Σ the following:

1. (Guess the Types) For each term, we guess its type in a certain chase interpretation via the disjunctive rule:

Notice that we assume, w.l.o.g., that for each term t occurring in a chase interpretation I, Term(t) occurs in I; this is a consequence of our normalization procedure. We also add, for each T ∈ 2S and R/k ̸∈ T :

4 This is not true if unguarded negative constraints occur in Σ.

to ensure that the guessing is correct. We also state that initially the partial type of a term is empty:

Finally, we need to guarantee that the types are actually encoding the relations that are realized in a chase interpretation. For each T ∈ 2S and relation R/k ∈ T :

and for each T1, T2 ∈ 2S such that T1 \ T2 = {R/k}:

1. (Construct the Representatives) We generate the auxiliary atoms that eventually will lead to the representatives for Cross atoms as follows. For each T1, . . . , T4 ∈ 2S such that T1 ⊆ T2 and T3 ⊆ T4:

1. (Type Propagation to Original Atoms) Finally, we need to propagate the derived types for the representative terms back to the original terms. For each T1, . . . , T6 ∈ 2S such that T1 ⊂ T5 ⊆ T2 and T3 ⊂ T6 ⊆ T4, we add:

This completes the construction of Σ+, and the desired ontology Σ′ = Σ+ \ {ϕcp}. Let S′ be the schema of Σ′ .

Lemma 4 It holds that (i) Σ and Σ′ are equisatisfiable, (ii) Σ′ can be constructed in exponential time, and (iii) max{k | R/k ∈ S} = max{k | R/k ∈ S′ }.

The above lemma, together with the fact that Sat(GF) is feasible in exponential time in the size of the ontology and the size of the schema, and in double-exponential time in the arity of the schema [Gr¨adel, 1999], implies that Sat(GF×2 ) is in 2EXPTIME, and Theorem 3 follows.

Let us conclude by saying that in the case of bounded arity relations the exact complexity of Sat(GF×2 ) is open. However, we can show that it is NEXPTIME-hard by exploiting the standard tiling problem for the exponential grid. This is an indication that (in the case of bounded arity) the presence of cross products increases the complexity since without cross products the problem is EXPTIME-complete [Gr¨adel, 1999].

5 Evaluation of (GF×,UCQ) Queries

We now focus on OMQ evaluation. Let us first observe that Eval(GF×3 ,UCQ) is at least as hard as Sat(GF×3 ). Indeed, given a GF×3 -ontology Σ, assuming that Q = (Σ, ∃xR(x)) and D = {P (c)}, where R and P do not occur in Σ, then Σ is unsatisfiable iff Q(D) ̸= ∅. This observation, together with Theorem 2, implies that Eval(GF×3 ,UCQ) is undecidable; in fact, the latter holds even for atomic queries. Thus, in order to obtain a positive result for OMQ evaluation, we should focus on GF×2 -ontologies. One may expect that Eval behaves like Sat, and the frontier between decidability and undecidability lies between (GF×2 ,UCQ) and (GF×3 ,UCQ). Unfortunately, Eval is more complex than Sat, and we can establish a strong negative result: OMQ evaluation remains undecidable even for (GF×2 2 ,CQ), where GF×2 2 denotes the two-variable fragment of GF×2 , that is, the set of GF×2 sentences that can mention at most two variables. It is apparent that for OMQ evaluation purposes, GF and cross products are incompatible. However, we can regain decidability by restricting either the query language and focus on acyclic UCQs, or the ontology language and concentrate on guarded existential rules. The rest of this section is devoted to discuss in more details the above results.

5.1 Evaluation of (GF×2 ,CQ) is Hard

We proceed to show that:

Theorem 5 Eval(GF×2 2 ,CQ) is undecidable, even if we focus on unary and binary relations.

The proof of the above result proceeds in two main steps:

1. We show that Eval(GF×2 2 ,UCQ) is undecidable by a reduction from the halting problem. Given a Turing machine M, we construct a database D, and an OMQ Q = (Σ, q) ∈ (GF×2 2 ,UCQ), where Σ mentions only unary and binary relations, such that M halts iff Q(D) ̸= ∅.
2. We then reduce Eval(GF×2 2 ,UCQ) to Eval(GF×2 2 ,CQ). It is known that such a reduction exists, which relies on the idea of encoding boolean operations via a set of database atoms; see, e.g., [Bourhis et al., 2016]. However, this technique increases the arity of the underlying schema and the number of variables by one. By exploiting the binary cross products, we can devise a reduction that preserves both the arity and the number of variables.

There is an easier way to establish Theorem 5 by exploiting the undecidability of OMQ evaluation under the two-variable fragment of first-order logic (FO2) [Rosati, 2007]. In particular, by exploiting the binary cross product, we can define the so-called universal role, that is, the binary relation interpreted as the cross product of the domain with itself. Then, we can use the universal role to convert every formula in FO2 into a formula in GF×2 2 . Nevertheless, we believe it is more insightful to provide a proof from first principles, which helps us to better understand the power of (GF×2 2 ,CQ).

5.2 Acyclic Queries

A well-behaved class of UCQs is the one based on acyclicity. A UCQ is acyclic if each of its disjuncts is acyclic, i.e., its hypergraph is acyclic [Chekuri and Rajaraman, 2000]. Let AUCQ be the class of acyclic UCQs. Then:

Theorem 6 Eval(GF×2 ,AUCQ) is 2EXPTIME-complete in the combined, and coNP-complete in the data complexity.

The above result relies on the fact that acyclic UCQs can be rewritten in linear time as UCQs that fall in GF. This allows us to use the construction underlying Theorem 3 in order to reduce Eval(GF×2 ,AUCQ) to Eval(GF,UCQ), and the desired upper bounds follow from Proposition 1. The lower bound for the combined complexity follows from the fact that Sat(GF) is 2EXPTIME-hard, while the coNP-hardness is implicit in [Calvanese et al., 2013].

5.3 Guarded Existential Rules

The other way to ensure decidability is by restricting the ontology language. We focus on guarded (non-disjunctive) existential rules. Recall that a rule ∀¯x∀¯ y(ϕ(¯x, ¯ y) → ∃¯ z ψ(¯x, ¯ z)) is guarded if ϕ has an atom that contains the variables (¯x∪ ¯ y). As said above, guarded rules do not directly fall in GF, but they can be transformed into GF sentences. We write GER×2 for the set of all guarded rules and binary cross products.

Theorem 7 Eval(GER×2 ,UCQ) is 2EXPTIME-complete in the combined, and PTIME-complete in the data complexity.

The fact that guarded existential rules do not permit disjunction in the right-hand side, allows us to devise a reduction from Eval(GER×2 , UCQ) to Eval(FGER, UCQ), where FGER is the class of frontier-guarded existential rules, that is, rules of the form∀¯x∀¯ y(ϕ(¯x, ¯ y) → ∃¯ z ψ(¯x, ¯ z)) with ϕ having an atom that contains all variables ¯x (instead of (¯x ∪ ¯ y)). This reduction exploits a simplified version of the construction underlying Theorem 3. The main reason why such a simplified version exists is because the (non-disjunctive) chase under GER×2 constructs a single interpretation (not a set of interpretations) that is a type invariant. Having the above reduction in place, the desired upper bounds are inherited from Eval(FGER,UCQ) [Baget et al., 2011], while the lower bounds are inherited from Eval(GER, CQ) [Cal`ı et al., 2013]. By following the same approach, we can show that Theorem 7 holds even if we consider the language (FGER×2 , UCQ).

6 Conclusions

Our main finding is that there are central guarded-based ontology languages that are compatible with binary cross products for satisfiability (e.g., the guarded fragment of first-order logic) and OMQ evaluation (e.g., (frontier-)guarded existential rules). An interesting research direction is to study query rewritabilty for the above ontology languages.

Acknowledgements

We would like to thank the anonymous reviewers for there useful comments. Bourhis is funded by CPER Nord-Pas de Calais/FEDER DATA Advanced data science and technologies 2015-2020 and the DeLTA project (ANR-16-CE400007). Morak is funded by the Austrian Science Fund (FWF), grant number Y698. Pieris is supported by the EPSRC Programme Grant EP/M025268/ "VADA: Value Added Data Systems - Principles and Architecture".