Finite Model Reasoning in Hybrid Classes of Existential Rules

1 Introduction

Rule-based languages lie at the core of knowledge representation and databases. In knowledge representation they are used for declarative problem solving, and, more recently, to model and reason about ontological knowledge, while in database applications they usually serve as expressive query languages that go beyond standard first-order queries. A prominent rulebased formalism is Datalog [Abiteboul et al., 1995]. Even though Datalog is quite powerful, with a variety of different applications, it is widely agreed that its inability to infer the existence of new values that are not already in the input database is a crucial limitation [Patel-Schneider and Horrocks, 2007]. Existential rules (a.k.a. tuple-generating dependencies and Datalog± rules), overcome this limitation by enriching Datalog with existential quantification in rule-heads. However, this leads to the undecidability of the main algorithmic tasks, and, in particular, of conjunctive query (CQ) answering [Beeri and Vardi, 1981; Cal`ı et al., 2013], i.e., the problem of checking whether a CQ is entailed by every model of an extensional database and a set of existential rules.

This negative outcome has led to a flurry of research activity for identifying restrictions on existential rules that ensure the decidability of query answering. Two such restrictions, which are of central importance for the present work, are guardedness [Baget et al., 2011; Cal`ı et al., 2013] and stickiness [Cal`ı et al., 2012]. It is well-known that guardedness is well-suited for forward reasoning, which in turn relies on the fact that guarded rules admit tree-like universal models. However, stickiness does not enjoy the above tree model property, and instead it relies on backward reasoning.

As one might expect, there are useful statements that can be expressed via guarded rules, but not with sticky rules, and vice versa. For example, using guarded rules we can state that the supervisor of a senior employee is also a senior employee, which is provably not expressible via sticky rules:

SeniorEmp(x), HasSupervisor(x, y) → SeniorEmp(y).

This rule is guarded since it has an atom in its body, called a guard, that contains x and y. However, using guarded rules we cannot say, e.g., that senior employees earn more money than junior employees. This is expressible via the sticky rule:

SeniorEmp(x), JuniorEmp(y) → MoreThan(x, y).

The goal of stickiness is to capture joins that are not expressible via guarded rules. This is done by forcing the join variables to be propagated to the inferred atoms. The above rule is trivially sticky since there are no join variables in its body.

It is a natural question to ask whether the above two inherently different classes of existential rules can be consolidated into a single formalism. This has been thoroughly investigated in [Gottlob et al., 2013]. It has been observed that the naive combination of guardedness and stickiness leads to the undecidability of query answering. This led to the notion of tameness, which provides an elegant and flexible way for taming the interaction between guarded and sticky rules. The essence of tameness is as follows: sticky rules are not allowed to trigger the guard of a guarded rule. It is easy to verify that the above two rules jointly satisfy the tameness condition.

Conjunctive query answering under the tamed combination of guardedness and stickiness is by now well-understood. A sophisticated hybrid query answering algorithm, which relies on a combination of forward and backward reasoning, has been devised in [Gottlob et al., 2013], which led to optimal complexity results: 2EXPTIME-complete in combined complexity, and PTIME-complete in data complexity. Notice that the analysis performed in [Gottlob et al., 2013] considers unrestricted models. However, in many KR applications the domain of interest is actually finite, and thus it is more realistic to reason over finite models. This has been already observed in the KR community, and there are several works that focus on finite model reasoning; see, e.g., [Amendola et al., 2017; Calvanese, 1996; Ib´a˜nez-Garc´ıa et al., 2014; Rosati, 2008]. Moreover, for intelligent database applications, the finiteness of the models is a key assumption. The question that comes up is whether finite query answering, i.e., query answering focussing on finite models, under tameness remains decidable, and, if this is the case, what is the exact complexity. Closing this non-trivial open problem is the main goal of this work.

The main outcome of our analysis is that finite query answering under tameness has the same complexity as (unrestricted) query answering. This is obtained by showing that the tamed combination of guardedness and stickiness enjoys finite controllability, i.e., finite and unrestricted query answering coincide. This exploits the fact that both guardedness and stickiness enjoy finite controllability [B´ar´any et al., 2014; Gogacz and Marcinkowski, 2017]. At this point, let us say that, in general, combining guardedness with unguarded classes of existential rules that are finitely controllable, by following the same approach as tameness, does not guarantee finite controllability. As we show later, there exist finitely controllable classes that their tamed combination with guardedness leads to classes that are not finitely controllable. Thus, to establish the above result, we need to perform a detailed model-theoretic analysis based on guardedness and stickiness. Our results can be summarized as follows:

• We first focus on a subclass of tame rules, obtained by posing a stratification condition on guarded and sticky rules, and show that is finitely controllable.
• ▶We then establish that a tame set of guarded and sticky rules can be rewritten as a stratified one that preserves finite answers, and thus tameness ensures finite controllability. This result immediately implies that finite query answering under tame guarded and sticky rules is 2EXPTIME-complete in combined complexity, and PTIME-complete in data complexity. The stratification relies on the fact that sticky rules are UCQ-rewritable. To establish the correctness of the stratification, we isolate a well-behaved family of finite models, called sticky-supported, that is a universal finite model set.
• Finally, triggered by the above construction, we study the relative expressive power among stratification and tameness. Interestingly, tame rules are more expressive than stratified rules w.r.t. the program expressive power [Arenas et al., 2014]. This essentially says that there is a tame set of guarded and sticky rules that cannot be expressed as a stratified set that gives the same answer for every database and CQ.

2 Preliminaries

Basics. Let C, N and V be disjoint countably infinite sets of constants, (labeled) nulls, and (regular) variables, respectively. The elements of (C∪N∪V) are also called terms. An atom is an expression of the form R(¯ t), where R is an n-ary predicate, and ¯ t = (t1, . . . , tn) are terms. A fact is an atom that contains only constants from C. A homomorphism from a set of atoms A to a set of atoms B is a mapping h from the terms in A to the terms in B, which is the identity on C, such that R(¯ t) ∈ A implies h(R(¯ t)) = R(h(¯ t)) ∈ B.

Databases and conjunctive queries. An instance is a (possibly infinite) set of atoms with constants and nulls, while a database is a finite set of facts. The active domain of an instance I, denoted dom(I), is the set of all terms in I.

A conjunctive query (CQ) is a formula of the formq(¯x) := ∃¯ y(R1(¯ v1) ∧ · · · ∧ Rm(¯ vm)), where each Ri(¯ vi) is an atom without nulls, 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. The evaluation of q(¯x) over I, denoted q(I), is defined as the set of tuples ¯ c ∈ C|¯x| for which there is a homomorphism h such that h(q(¯x)) ⊆ I and h(¯x) = ¯ c. Notice that, by abuse of notation, we sometimes treat a conjunction of atoms as a set of atoms. A union of conjunctive queries (UCQ) is a formula q(¯x) := ∨1≤i≤n qi(¯x), where each qi(¯x) is a CQ. The evaluation of q(¯x) over I, denoted q(I), is the set of tuples of constants ∪1≤i≤n qi(I).

Tuple-generating dependencies. A tuple-generating dependency (TGD) (a.k.a. existential rule) is a sentence of the form ∀¯x∀¯ y(ϕ(¯x, ¯ y) → ∃¯ z ψ(¯x, ¯ z)), where ϕ, ψ are (non-empty) conjunctions of atoms without constants and nulls. We write this TGD as ϕ(¯x, ¯ y) → ∃¯ z ψ(¯x, ¯ z), and use comma instead of ∧ for joining atoms. We call ϕ and ψ the body and head of the TGD, respectively. An instance I satisfies the TGD σ above, written I |= σ, if, whenever there is a homomorphism h such that h(ϕ(¯x, ¯ y)) ⊆ I, then there is h′ that agrees with h on ¯x such that h′ (ψ(¯x, ¯ z)) ⊆ I. The instance I satisfies a set Σ of TGDs, written I |= Σ, if I |= σ for each σ ∈ Σ. Let TGD be the class of finite sets of TGDs. Let us clarify that in the rest of the paper we work only with finite sets of TGDs.

Query answering under TGDs. For a database D and a set Σ of TGDs, a model of D and Σ is an instance I ⊇ D such that I |= Σ. Let fmods(D,Σ) and mods(D,Σ) be the set of finite and unrestricted models of D and Σ. The finite certain answers to a CQ q w.r.t. D and Σ is certfin(q,D, Σ) = ∩I∈fmods(D,Σ) q(I). We also define the certain answers to q w.r.t. D and Σ, denoted cert(q,D, Σ), where we consider models from mods(D,Σ). Recall that cert(q,D,Σ) coincides with the evaluation of q over chase(D, Σ), i.e., the (possibly infinite) instance constructed by the well-known chase procedure on D and Σ; see, e.g., [Cal`ı et al., 2013].

Our main problem in this work is to compute the finite certain answers to a CQ w.r.t. a database and a set of TGDs that falls in a certain class C, i.e., C ⊆ TGD; concrete classes of TGDs are given below. As is customary when studying the complexity of this problem, we focus on its decision version:

PROBLEM : FinQAns(C)

INPUT :

A database D, a set Σ ∈ C of TGDs,

a CQ q(¯x), and a tuple ¯ c ∈ dom(D)|¯x| .

QUESTION : Does ¯

c ∈ certfin(q, D, Σ)?

We also refer to QAns(C), which is defined as above with the difference that we ask whether ¯ c belongs to cert(q, D, Σ). For both problems, we use the standard complexity measures, i.e., combined complexity and data complexity.

Concrete classes of TGDs. It is well-known that both FinQAns(TGD) and QAns(TGD) are undecidable problems. This has led to a flurry of activity for identifying restrictions on TGDs that make the above problems decidable. Here, we concentrate on a class obtained by combining two of the main decidability paradigms, i.e., guardedness and stickiness.

Guardedness: A TGD is called guarded if it has a body atom, called guard, that contains all the body variables [Cal`ı et al., 2013]. Let G be the class of sets of guarded TGDs.

Stickiness: The goal of stickiness is to capture joins that are not expressible via guarded TGDs. The key idea can be described as follows: variables that appear more than once in the body of a TGD should be inductively propagated (or "stick") to the head atoms. The definition is based on an inductive procedure that marks the variables that violate the above property. Consider a set Σ of TGDs. During the base step, a variable that appears in the body of a TGD of Σ but not in its head is marked. Now, if a variable x in the head of a TGD σ ∈ Σ appears at position R[i] (i.e., the i-th attribute of the predicate R), and there exists some σ′ ∈ Σ that has in its body at position R[i] a marked variable, then x in the body of σ is marked. We say that Σ is sticky if every marked variable appears only once in the body of a TGD. For more details see [Cal`ı et al., 2012]. Let S be the class of sticky sets of TGDs.

Guardedness + Stickiness: The notion of tameness has been introduced in [Gottlob et al., 2013], with the aim of taming the interaction between guarded and sticky TGDs. The idea is to allow guarded and sticky TGDs to co-exist as long as none of the sticky TGDs triggers the guard of a guarded TGD. Before we give the formal definition, we need to recall two auxiliary notions. A set Σ of TGDs belongs to the union of G and S, denoted G|S, if there is a partition {Σg, Σs} of Σ such that Σg ∈ G and Σs ∈ S. A guard function of a set Σ ∈ G is a function g from Σ to the set of atoms in Σ such that: for each σ ∈ Σ, g(σ) is an atom in the body of σ that contains all its body variables. In other words, a guard function specifies which body atom plays the role of the guard.

We can now recall tameness. A set Σ of TGDs is GS-tame if Σ ∈ G|S, and there exists a partition {Σg, Σs} of Σ, with Σg ∈ G and Σs ∈ S, such that: there exists a guard function g of Σg such that, for every σ ∈ Σg, the predicate of g(σ) does not occur in the head of a TGD of Σs. In simple words, Σ is GS-tame if it can be partitioned into a guarded component Σg and a sticky component Σs, and, in addition, we can choose the guards of Σg in such a way that none of their predicates appears in the head of a sticky TGD. The obtained class is denoted G|tS, where |t denotes the fact that we consider the union of G and S, but with tamed interaction. It is known that QAns(G|tS) is 2EXPTIME-complete in combined complexity, and PTIME-complete in data complexity [Gottlob et al., 2013]. However, the complexity of FinQAns(G|tS) is still open. Closing this problem is the main goal of this work.

3 Finite Controllability

A key notion for our analysis is finite controllability [Rosati, 2011]. We say that a class C of TGDs is finitely controllable if, for every database D, set Σ ∈ C of TGDs, and CQ q, certfin(q,D,Σ) = cert(q,D,Σ). This suggests that, for pinpointing the complexity of FinQAns(C), where C is finitely controllable, it suffices to focus on QAns(C). As already said, the complexity of QAns(G|tS) is known. Therefore, our goal is to show that G|tS is finitely controllable, which will immediately give us the complexity of FinQAns(G|tS). To this end, we are going to exploit the fact that both G and S are finitely controllable. For G, this has been shown in [B´ar´any et al., 2014], while for S in [Gogacz and Marcinkowski, 2017].

Tameness vs. finite controllability. At this point, one may be tempted to think that, since both G and S are finitely controllable, it is straightforward to show that also G|tS is finitely controllable. In other words, one may claim that tameness preserves finite controllability, no matter which finitely controllable class of TGDs we consider in the place of stickiness. We proceed to show that this is not the case.

It should be clear by now that tameness provides a generic way for combining guardedness with other unguarded classes of TGDs. Thus, in the same way as G|tS, we can define G|tC, where C is some arbitrary class of TGDs. We now show that there is a finitely controllable class C of TGDs such that G|tC is not finitely controllable. To achieve this, we are going to consider the class of full TGDs, i.e., TGDs without existentially quantified variables; we denote this class by F. It is immediate that F is finitely controllable, since the chase procedure terminates; see, e.g., [Fagin et al., 2005]. However:

Proposition 1 G|tF is not finitely controllable.

Proof (sketch). Let D = {P(a, b),R(a, b)}, and Σ ∈ G|tF the set of TGDs consisting of

Every I ∈ fmods(D, Σ) contains an atom of the form R(t, a), where t is some term. However, chase(D,Σ) does not contain such an atom. Therefore, assuming that q is the Boolean CQ ∃xR(x, a), () ∈ certfin(q,D, Σ) and () ̸∈ cert(q,D, Σ); () is the empty tuple. The claim follows.

The above result suggests that using blindly the fact that both G and S are finitely controllable, without exploiting any additional property, it is not enough for establishing that G|tS is finitely controllable. This indicates that a detailed analysis is required. The next two sections are devoted to performing this analysis, and showing that G|tS is finitely controllable.

4 The Stratified Case

We first focus on a simpler class of TGDs and show that is finitely controllable. This result is interesting in its own right, but, more crucially, it provides a useful tool that we are going to exploit for showing that G|tS is finitely controllable.

This simpler class of TGDs is obtained by limiting the interaction between guardedness and stickiness via stratification. A set Σ of TGDs is GS-stratified if Σ ∈ G|S, and there exists a partition {Σg, Σs} of Σ, where Σg ∈ G and Σs ∈ S, such that: for every σ ∈ Σg, none of the predicates in the body of σ occurs in the head of a TGD of Σs. We write G|sS for the obtained class. Clearly, G|sS ⊂ G|tS. We show that:

Theorem 2 G|sS is finitely controllable.

Before giving the proof, we need to recall that S is UCQrewritable [Cal`ı et al., 2012]. This means that, for a set Σ ∈ S of TGDs and a CQ q, we can always construct a (finite) UCQ qΣ such that, for every database D, cert(q, D, Σ) = qΣ(D).

Proof. Consider a set Σ ∈ G|sS. We need to show that, for every database D and CQ q, certfin(q, D, Σ) = cert(q, D, Σ). It is clear that cert(q,D,Σ) ⊆ certfin(q,D,Σ); thus, it remains to show that certfin(q, D, Σ) ⊆ cert(q, D, Σ).

Let {Σg, Σs}, where Σg ∈ G and Σs ∈ S, be a partition of Σ that witnesses the fact that Σ ∈ G|sS. We are going to show that, for an arbitrary tuple ¯ c of constants, ¯ c ̸∈ cert(q,D,Σ) implies ¯ c ̸∈ certfin(q,D,Σ). Before we proceed further, let us state an auxiliary lemma, which establishes a useful connection between the models of Σg and Σs:

Lemma 3 Fix an instance I ∈ mods(D, Σg). For every J ∈ mods(I, Σs), there is K ⊆ J such that K ∈ mods(D, Σ).

We are now ready to complete the proof of Theorem 2:

• ¯ c ̸∈ cert(q, D, Σ) (by hypothesis)
• ⇒ there exists a UCQ qΣs such that ¯ c ̸∈ cert(qΣs , D, Σg) (by UCQ-rewritability of S, and GS-stratification)
• ⇒ ¯ c ̸∈ certfin(qΣs , D, Σg) (by finite controllability of G)
• ⇒ there exists I ∈ fmods(D,Σg) such that ¯ c ̸∈ qΣs (I)
• ⇒ ¯ c ̸∈ cert(q, I, Σs)
• (since qΣs is a UCQ-rewriting of Σs and q)
• ⇒ ¯ c ̸∈ certfin(q, I, Σs)
• (by finite controllability of S)
• ⇒ there exists J ∈ fmods(I,Σs) such that ¯ c ̸∈ q(J)
• ⇒ there exists K ⊆ J such that K ∈ fmods(D,Σ) (by Lemma 3)
• ⇒ ¯ c ̸∈ q(K) (by monotonicity of CQs)
• ⇒ ¯ c ̸∈ certfin(q, D, Σ),

as needed. This completes our proof.

It is interesting to observe that in the above proof, we only use the fact that G and S are finitely controllable, and also the fact that S is UCQ-rewritable. This suggests that actually Theorem 2 can be extended to any class of TGDs C1|sC2 (defined in the same way as G|sS) as long as C1 and C2 are finitely controllable, and C2 is UCQ-rewritable. This result is of independent interest, which can be a useful tool for identifying even more expressive finitely controllable classes.

5 The Tamed Case

We now proceed with our main technical result:

Theorem 4 G|tS is finitely controllable.

As a corollary to Theorem 4 we obtain the following result:

Corollary 5 FinQAns(G|tS) is complete for 2EXPTIME in combined complexity, and PTIME in data complexity The rest of this section is devoted to explaining the proof of Theorem 4. Fix Σ ∈ G|tS. We need to show that, for every database D and CQ q, certfin(q, D, Σ) = cert(q, D, Σ). Since cert(q,D,Σ) ⊆ certfin(q,D,Σ) holds trivially, it remains to show that certfin(q, D, Σ) ⊆ cert(q, D, Σ). Our plan of attack for showing the latter containment is as follows. We are going to convert Σ into a set Σ⋆ ∈ G|sS, i.e., into a GS-stratified set of TGDs, and q into a CQ q⋆ , such that:

1. certfin(q,D,Σ) ⊆ certfin(q⋆ ,D,Σ⋆ ).
2. cert(q⋆ ,D,Σ⋆ ) ⊆ cert(q,D,Σ).

It is then easy, by exploiting also the fact that G|sS is finitely controllable, to establish the desired containment:

In the rest of this section, we explain how Σ⋆ and q⋆ are constructed, and show the containments (1) and (2) above.

Constructing Σ⋆ and q⋆

The construction of the set Σ⋆ proceeds in three main steps. Let {Σg, Σs}, where Σg ∈ G and Σs ∈ S, be the partition of Σ that witnesses the fact that Σ ∈ G|tS:

Enriching step. We enrich the set Σg in such a way that we obtain a set Σ+g ∈ G that is powerful enough to entail all the atoms that are entailed by Σs and affect Σg. This is the most crucial and complex step in the construction of Σ⋆ , for which details are given below.

Copying step. We construct a set Σc of "copy" TGDs, which essentially copies each predicate P occurring in Σ+g into a fresh predicate P ⋆ . Formally, for each n-ary predicate P occurring in Σ+g , Σc contains the TGD:

Stratification step. We construct the set of TGDs Σ⋆ by taking the union Σ+g ∪Σc ∪Σ⋆s , where Σ⋆s is obtained from Σs by renaming each predicate P to P ⋆ .

It is clear that Σ⋆ falls in G|sS since none of the "star" predicates in the head of a TGD of Σ⋆s ∈ S occurs in the body of a TGD of (Σ+g ∪Σc) ∈ G. Now, having Σ⋆ in place, it should be clear that q⋆ is the CQ obtained from q by renaming each predicate P to P ⋆ . Let us now formalize the enriching step.

Formalization of the enriching step. This step relies on the notion of embedding of Σs into a TGD σ ∈ Σg, which hinges on the fact that S is UCQ-rewritable. Roughly, we see the body of σ as a CQ qσ , and we consider the UCQ-rewriting of qσ with Σs. Each partial rewriting gives rise to a new TGD, which in turn can be transformed into linearly many guarded TGDs. The obtained set of guarded TGDs is the embedding of Σs into σ, denoted Embed(Σs, σ). Having this in place, we can then construct the enriched version of Σg by embedding Σs into every TGD σ ∈ Σg, i.e.,

It remains to formalize the embedding of Σs into σ. Let us assume that the TGD σ ∈ Σg is of the formR(¯x, ¯ y), φ(¯x, ¯ y) → ∃¯ zψ(¯x, ¯ z), where R(¯x, ¯ y) is the guard of σ provided by the guard function g of Σg. Let qσ (¯x) be the CQ

By employing the resolution-based query rewriting algorithm from [Gottlob et al., 2014], we can construct a finite UCQrewriting of qσ and Σs, denoted qσΣs , such that, each CQ q of qσΣs enjoys two useful syntactic properties: (i) q is answerguarded, i.e., it has an atom that contains all the free variables of q, while the answer-guard is ρq(R(¯x, ¯ y)), where ρq is some mapping that maps the variables in q to variables in q, and (ii) for each variable x in q, if x does not occur in qσ , then x occurs only once in q. Having qσΣs in place, we define

i.e., each CQ q in qσΣs becomes the body of a TGD τq, while the head of τq is the head of the input TGD σ after applying the mapping ρq to the variables of ¯x. Notice that the TGDs of Tσ are not guarded. However, since each q in qσΣs is answerguarded, with ρq(R(¯x, ¯ y)) being the answer-guard, τq enjoys the following property: the body atom ρq(R(¯x, ¯ y)) of τq contains all the variables that appear both in the body and in the head of τq, while each other variable that appears in the body but not in the head, occurs only once in the body of τq. Notice that the set of body variables of a TGD that occur also in the head is known as the frontier of the TGD. Thus, in what follows, we refer to the atom ρq(R(¯x, ¯ y)) in the body of τq as the frontier-guard of τq. The above property of τq allows us to convert it into linearly many guarded TGDs.

Consider a TGD τ ∈ Tσ, and an atom α = S(x1, . . . , xn) in its body with xi1 , . . . , xik being the variables in α that occur also in the frontier-guard of τ. We write p(α) for the atom Sα τ (xi1 , . . . , xik ), where Sα τ is an auxiliary predicate, and p(τ) for the TGD obtained from τ after replacing each body atom α of τ, other than the frontier-guard, with p(α). We also denote by σα τ the TGD

which simply computes the projection of S over i1, . . . , ik. For brevity, we say that an atom in the body of a TGD τ ∈ Tσ is a side-atom if it is not the frontier-guard of τ . We can now easily convert Tσ into a set of guarded TGDs, which gives us the embedding of Σs into σ:

This completes the formalization of the enriching step.

Establishing the crucial containments

We proceed to show the crucial containments that, together with Theorem 2, allow us to conclude Theorem 4.

Consider a tuple of constants ¯ c. We proceed to show that if ¯ c ̸∈ certfin(q⋆ ,D,Σ⋆ ), then ¯ c ̸∈ certfin(q,D, Σ). Our plan of attack for showing this is as follows:

• We isolate a class of finite models of D and Σ⋆ , the socalled sticky-supported (or s-supported), and show that it forms a universal finite model set, i.e., for every I ∈ fmods(D,Σ⋆ ), there exists J ∈ fmods(D,Σ⋆ ) that is s-supported and can be homomorphically mapped to I.
• Since ¯ c ̸∈ certfin(q⋆ ,D, Σ⋆ ), there exists an s-supported I ∈ fmods(D, Σ⋆ ) such that ¯ c ̸∈ q⋆ (I). We finally show that the instance J obtained from I by renaming each predicate P ⋆ into P, is a finite model of D and Σ such that ¯ c ̸∈ q(J). Thus, ¯ c ̸∈ certfin(q, D, Σ).

We proceed to formalize the above description.

Sticky-supported models. The definition of s-supported models relies on the disjunctive chase introduced in [Deutsch and Tannen, 2003], an extension of the chase procedure that is able to deal with disjunctive TGDs (DTGD), i.e., TGDs extended with disjunction in the head. Each disjunctive chase step "branches" out several instances, each satisfying one of the disjuncts of the DTGD that is applied. Thus, the result of the disjunctive chase is, in general, a set of instances (and not a single instance as in the classical chase). For a set of DTGDs Σ∨, we write dchase(D, Σ∨) for the result of the disjunctive chase of D w.r.t. Σ∨. Before introducing s-supported models, we need some auxiliary terminology.

We assume that the TGDs of Σ⋆s have only one atom in the head, which contains at most one occurrence of an existentially quantified variable. This does not affect the generality of our proof, since the normalization procedure from [Cal`ı et al., 2012], which converts a TGD into linearly many TGDs with the above properties, preserves finite certain answers. For a (finite) set of nulls N = {⊥1, . . . ,⊥n} ⊂ N, where n ≥ 1, we define ∨N(Σ⋆s ) as the set of DTGDs obtained from Σ⋆s by instantiating the existentially quantified variables using nulls fromN. For example, if N = {⊥1, ⊥2}, the TGD R⋆ (x, y) → ∃z S⋆ (y, z) will be transformed into the DTGD R⋆ (x, y) → S⋆ (y, ⊥1) ∨ S⋆ (y, ⊥2). For I ∈ fmods(D, Σ⋆ ),

We now define s-supported models.

Definition 6 We say that I ∈ fmods(D, Σ⋆ ) is s-supported if

Intuitively speaking, I is s-supported if S⋆ (I) can be obtained starting from G⋆ (I) and executing the TGDs of Σ⋆s in a chase-like manner, but the existentially quantified variables are satisfied by nulls of dom(I) that do not occur in G⋆ (I). Notice the crucial difference with the standard chase procedure, where an existentially quantified variable is always satisfied by a "fresh" null, which may lead to an infinite instance. We now show the following crucial result:

Lemma 7 The set {I ∈ fmods(D,Σ⋆ ) | I is s-supported} is a universal finite model set of D and Σ⋆ .

Proof (sketch). Fix an arbitrary I ∈ fmods(D, Σ⋆ ). We have to show that there exists an instance from fmods(D, Σ⋆ ) that is s-supported, and it can be homomorphically mapped to I. To this end, we first show that there exists an instance J from dchase(G⋆ (I), ∨N(Σ⋆s )), with N = {⊥1, . . . , ⊥|dom(I)|} and N ∩ dom(G⋆ (I)) = ∅, and a homomorphism h such that h(J) ⊆ (G⋆ (I) ∪ S⋆ (I)). Let dom(G⋆ (I)) = {t1, . . . , tn}, and dom(I) \ dom(G⋆ (I)) = {u1, . . . , um}. We define h as

We can show, by induction on the number of disjunctive chase steps, that indeed there exists J ∈ dchase(G⋆ (I), ∨N(Σ⋆s )) such that h(J) ⊆ (G⋆ (I)∪S⋆ (I)). Observe now that (G(I)∪ J) ∈ fmods(D, Σ⋆ ), is s-supported, and h(G(I) ∪J) ⊆ I.

The countermodel of D and Σ. Lemma 7 implies that there exists an s-supported I ∈ fmods(D, Σ⋆ ) such that ¯ c ̸∈ q⋆ (I). We claim that GS(I) = (G(I) ∪ S(I)), where S(I) is obtained from S⋆ (I) after renaming each predicate P ⋆ to P, is the desired countermodel of D and Σ. More precisely:

Proof (sketch). It is clear that GS(I) ⊇D and GS(I) |= Σs. Moreover, since q is q⋆ after renaming each predicate P ⋆ to P, ¯ c ̸∈ q(GS(I)). Thus, it remains to show that GS(I) |= Σg. Consider an arbitrary TGD σ ∈ Σg of the form φ(¯x, ¯ y) → ∃¯ z ψ(¯x, ¯ z), and assume there is a homomorphism h such that h(φ(¯x, ¯ y)) ⊆ GS(I). We need to show that there is h′ that agrees with h on ¯x such that h′ (ψ(¯x, ¯ z)) ⊆ GS(I). Due to tameness, the guard of σ provided by the guard function of Σg is mapped by h to G(I). This implies that h(φ(¯x, ¯ y)) contains only terms from dom(G(I)). Let us consider h(φ(¯x, ¯ y)) as a Boolean CQ, denoted qσ h ; by abuse of terminology, qσ h contains null values from dom(G(I)), which should be interpreted as constants. We proceed to establish a crucial claim:

Proof (sketch). The claim is equivalent to h(φ(¯x, ¯ y)) ⊆ chase(G(I),Σs). Let φ⋆ (¯x, ¯ y) be the conjunction of atoms obtained from φ(¯x, ¯ y) by renaming each predicate P to P ⋆ . It is clear that h(φ⋆ (¯x, ¯ y)) ⊆ (G⋆ (I) ∪ S⋆ (I)), which implies that there exists J ∈ dchase(G⋆ (I), ∨N(Σ⋆s )), where N = {⊥1, . . . ,⊥|dom(I)|} and N ∩ dom(G⋆ (I)) is empty, such that h(φ⋆ (¯x, ¯ y)) ⊆ J. Therefore, there exists a finite sequence of disjunctive chase steps, starting from G⋆ (I) and applying the DTGDs of ∨N(Σ⋆s ), that generates h(φ⋆ (¯x, ¯ y)). Crucially, none of these steps performs a join over a null of N, i.e., at each step, the variables that occur more than once in the body of the applied DTGD are mapped to terms of dom(G⋆ (I)); otherwise, Σ⋆s is not sticky. This allows us to extract from the above sequence of disjunctive chase steps, a finite sequence of standard chase steps, starting from G⋆ (I) and applying TGDs of Σ⋆s , that generates h(φ⋆ (¯x, ¯ y)). Therefore, h(φ⋆ (¯x, ¯ y)) ⊆ chase(G⋆ (I),Σ⋆s ), which immediately implies that h(φ(¯x, ¯ y)) ⊆ chase(G(I), Σs), as needed.

The above claim implies that there exists a partial rewriting q of qσ h and Σs, and a homomorphism µ that extends h, such that µ(q) ⊆ G(I). This fact allows us to show that there is

σ+ ∈ Embed(Σs, σ) such that h maps the body of σ+ to G(I). Since G(I) |= Embed(Σs, σ), there exists h′ , which agrees with h on ¯x, that maps the head of σ+ to G(I). Thus, h′ (ψ(¯x, ¯ z)) ⊆ GS(I), and the claim follows.

It is clear that Lemma 8 implies that ¯ c ̸∈ certfin(q,D,Σ), and containment (1) follows.

Containment 2: cert(q⋆ ,D,Σ⋆ ) ⊆ cert(q,D,Σ)

Consider a tuple ¯ c of constants. We proceed to show that, if ¯ c ∈ cert(q⋆ ,D,Σ⋆ ), then ¯ c ∈ cert(q,D,Σ). Although the proof of this implication is not straightforward, it is simpler than the proof of containment (1) since we deal with certain answers (not finite certain answers). This allows us to exploit the soundness of the UCQ-rewritings underlying the construction of Σ⋆ in a direct way.

Let chase(D,Σ⋆ )-⋆ be the chase instance of D and Σ⋆ after renaming each predicate P ⋆ to P. Then:

Lemma 9 There exists a homomorphism h such that h(chase(D,Σ⋆ )-⋆ ) ⊆ chase(D,Σ).

By hypothesis, ¯ c ∈ q⋆ (chase(D,Σ⋆ )), which in turn implies that ¯ c ∈ q(chase(D,Σ⋆ )-⋆ ). By Lemma 9 we get that ¯ c ∈ q(chase(D, Σ)), and containment (2) follows.

6 Relative Expressive Power

We have seen that, given a set Σ ∈ G|tS and a CQ q, it is always possible to construct a set Σ⋆ ∈ G|sS and a CQ q⋆ such that, for every database D, cert(q,D,Σ) = cert(q⋆ ,D,Σ⋆ ). Let us clarify that in this section we focus on (arbitrary) certain answers since G|tS and G|sS are finitely controllable. At this point, one may be tempted to think that G|tS and G|sS are equally expressive. However, whenever we refer to the expressive power of a class of existential rules, we are usually interested in the so-called program expressive power [Arenas et al., 2014], which aims at the decoupling of the set of TGDs from the CQ. Let us recall the formal definition.

Consider a set Σ of TGDs. The program expressive power of Σ, denoted pep(Σ), is the set of triples (D, q, ¯ c), where D is a database, q(¯x) is a CQ, and ¯ c belongs to cert(q,D,Σ). Then, the program expressive power of a class C is defined as pep(C) = {pep(Σ) | Σ ∈ C}. A class C is more expressive than a class C′ , written C′ ≺ C, if pep(C′ ) ⊂ pep(C). It is not difficult to show that C is more expressive than C′ iff:

1. For every Σ′ ∈ C′ , there exists Σ ∈ C such that, for every D and q, cert(q, D, Σ) = cert(q, D, Σ′ ).
2. There exists Σ ∈ C such that, for every Σ′ ∈ C′ , there exists D and q such that cert(q, D, Σ) ̸= cert(q, D, Σ′ ).

It is clear that the construction given in the previous section does not show that G|tS and G|sS have the same program expressive power since we modify the CQ (we rename each predicate P to P ⋆ ). Even though this is a mild modification, it turned out that is unavoidable. We can show that:

Theorem 10 G|sS ≺ G|tS.

Proof (sketch). We need to show pep(G|sS) ⊂ pep(G|tS). Clearly, pep(G|sS) ⊆ pep(G|tS) since G|sS ⊂ G|tS. It remains to show that there exists Σ ∈ G|tS such that pep(Σ) ̸∈

pep(G|sS), or, equivalently, for every Σ′ ∈ G|sS, there exists D and q such that cert(q,D,Σ) ̸= cert(q,D,Σ′ ). Let Σ be the set consisting of the TGDs

Assume there exists Σ′ ∈ G|sS such that cert(q,D,Σ) = cert(q, D, Σ′ ) for every D and q. If {Σ′g , Σ′s }, where Σ′g ∈ G and Σ′s ∈ S, is the partition of Σ′ that witnesses the fact that Σ′ ∈ G|sS, we can show that Σ′s ̸∈ S, which is a contradiction. To show this, we employ the database

and the CQ q = R(c2, c5). The proof exploits the fact that, during the chase, guarded TGDs cannot propagate in an atom two constants that are not already together in a database atom, which implies that R(c2, c5) is generated by a TGD of Σ′s . We also use the fact that S is UCQ-rewritable, and, in particular, the fact that in each partial rewriting of q and Σ′s , "fresh" variables occur only once due to stickiness.

7 FutureWork

Although the problem of checking whether a tuple is a certain answer has attracted considerable attention, the problem of checking whether a tuple is not a certain answer has received far less attention. By exploiting the ideas underlying s-supported models, we are planning to devise algorithms that will try to refute a candidate certain answer, assuming that the input set of TGDs is finitely controllable, by first exploring finite models with only one null, and then incrementally explore finite models with more nulls. If a candidate is not certain, then this procedure will recognize it since it explores a universal finite model set. Such an algorithm can be executed in parallel with the chase procedure, which can be used for checking whether a candidate answer is entailed. Therefore, we obtain a sound and complete procedure for query answering under finitely controllable classes of TGDs. We believe that such a parallel procedure can lead to practical algorithms since in real-life scenarios the entailment or refutation of a candidate answer can be recognized quickly without introducing a prohibitively large number of nulls.

Acknowledgements

Gottlob and Pieris have been supported by the EPSRC Programme Grant "VADA" EP/M025268/. Manna has been partially supported by the Italian Ministry for Economic Development under PON project "S2BDW" (n. F/050389/0103/X32), and by Regione Calabria under POR project "DLV Large Scale" (CUP J28C17000220006).