The chase procedure was initially developed for testing logical implication
between sets of dependencies [
Since the chase procedure was first adopted for data exchange one of the main problems was whether it terminates in a finite number of steps. Clearly, when considering only source to target dependencies the chase procedure terminates, as there is no recursion involved. Unfortunately, adding even simple target constraints may lead to non-termination. For example, consider the data exchange setting given by one source to target dependency ∀x, y ∶ S(x, y) → R(x, y), the target dependency ∀x, y ∶ R(x, y) → ∃z R(y, z), and the source instance I = {S(a, b)}. It is easy to see that chasing I with the given dependencies is nonterminating, as at each step the target dependency will generate a new tuple, containing a fresh new labeled null, and that this new tuple will cause the target dependency to fire again.
This leads to a fundamental question: ”When does the chase terminate?”
This question was shown to be undecidable Deutsch et al. in [
In this paper we show that our conditional chase is guaranteed to terminate
for the richly acyclic dependencies introduced by Hernich and Schweikardt [
⋆
The rest of this paper is organized as follows. In Section 2 we introduce basic notions used throughout the paper. In Section 3 we describe the constructible solutions semantics and the conditional chase procedure. Then, in Section 4 we show that the conditional chase with richly acyclic sets of dependencies is guaranteed to terminate. Conclusions are drawn in the last section. 2
For required background knowledge the reader should consult [
Relational instances. Let Cons be a countably infinite set of constants, usually denoted a, b, c, . . ., possibly subscripted. From the domain Cons and a finite set R of relation names, we build up a Herbrand structure consisting of all expressions of the form R(a1, a2, . . . , ak), where R is a “k-ary” relation name from R, and the ai’s are values in Cons. Such expressions are called ground atoms, or ground tuples. A database instance I is then simply a finite set of ground tuples, e.g. {R1(a1, a3), R2(a2, a3, a4)}. We denote the set of constants occurring in an instance I with d om(I).
Relational tableaux. Let Vars be a countably infinite set, disjoint from the set of constants. Elements in Vars are called variables, and are denoted X, Y, Z, . . ., possibly subscripted. We can then also allow non-ground atoms, i.e. expressions of the form R(a, X, b, . . . , X, Y ). A tableau T is a finite set of atoms (ground, or non-ground). A non-ground atom represents a sentence where the variables are existentially quantified. The set of variables and constants in a tableau is denoted d om(T ).
Let T and U be tableaux. A mapping h from d om(T ) to d om(U ), that is the identity on Cons, extended component-wise, is called a homomorphism from T to U if h(T ) ⊆ U . If there is an injective homomorphism h such that h(T ) = U , and the inverse of h is a homomorphism from U to T , we say that T and U are isomorphic. An endomorphism on a tableau T is a mapping on d om(T ) such that h(T ) ⊆ T . Finally, a valuation is a homomorphism whose image is contained in Cons.
Tuple generating dependencies. A tuple generating dependency (tgd) is a first order formula of the form
∀x ∶ α(x, y) → ∃z β(x, z) where α is a conjunction of atoms, β is a single atom1, and x,y and z are sequences of variables. We assume that the variables occurring in dependencies are disjoint from all variables occurring in any tableaux under consideration. To emphasize this, we use lowercase letters for variables in dependencies. When α is the antecedent of a tgd, we shall sometimes conveniently regard it as a tableau, and refer to it as the body of the tgd. Similarly we refer to β as the head of the tgd. If there are no existentially quantified variables the dependency is said to be full, otherwise it is embedded. Frequently, we omit the universal quantifiers in tgd formulae. Also, when the variables are not relevant in the context, we denote a tgd α(x, y) → ∃z β(x, z) simply as α → β.
Let ξ = α → β be a tuple generating dependency, and I an instance. Then we say that I satisfies ξ, if I ⊧ ξ in the standard model theoretic sense, or equivalently, if for every homomorphism h, such that h α ( ) ⊆ I, there is an extension h′ of h, such that h′(β) ∈ I.
The standard chase. The standard chase works on tableaux. Let Σ be a set of tgd’s and T a tableau. A trigger for Σ on T is a pair (ξ, h), where ξ = α → β ∈ Σ, and h is a homomorphism such that h(α) ⊆ T . The set of all triggers for Σ on T is denoted t riggΣ (T ). It is easy to see that t riggΣ (T ) is finite.
A trigger (ξ, h) ∈ t riggΣ (T ), with ξ = α → β, is said to be active if there is no
extension h′ of for which h′(β) ∈ T . The standard chase step [
Deutsch et al. [
Then a tableau T is said to satisfy a set Σ of dependencies, if I ⊧ Σ, for all
I ∈ Rep(T ). A tableau U = C hasesΣtand(T ) is indeed a universal model for T ∪ Σ,
but there can be ground instances in Rep(U ) that do not satisfy Σ. For
instance, let T = {R(a, b), R(X, c)}, and Σ = {R(x, y), R(y, z) → S(x, z)}. Then
C hasesΣtand(T ) = T , I = {R(a, b), R(b, c)} ∈ Rep(T ), but I ⊧~ Σ. Consider now
the nonmonotonic Boolean query R(a, b) ∧ ¬S(a, c). Evaluated on T the certain
answer will be true, which clearly should not be the case, as the query evaluates
to false on the instance I ∪ {S(a, c)}, and I ∪ {S(a, c)} is a model of T ∪ Σ.
In [
Constructible models. Let I be a ground instance and Σ a set of tgd’s.
Consider a chase step on I with a tgd ξ = α(x, y) → ∃z β(x, z), and trigger (ξ, h).
Instead of adding the tuple β(h(x), Z′), where Z′ is a sequence of new fresh
variables, we create a branch for each sequence c of constants and add the ground
tuple β(h(x), c) to I. Continuing in this fashion we will have a chase tree,
instead of a chase sequence. Notably, all nodes in the tree will be ground instances.
The leaves of the chase tree form the set of constructible models of I and Σ,
denoted Σ(I). If the initial input to the chase is a tableau T , the constructible
Conditional tables. A conditional table (c-table) [
The set of possible worlds represented by (T, ϕ) is
Rep(T, ϕ) = {v(T, ϕ) ∶ v is a valuation }.
Unifiers. Let T and U be tableaux. A unifier for T and U , if it exists, is a pair
(θ1, θ2), where θ1 is a homomorphism from d om(T ) to d om(U ), and θ2 is an
endomorphism on d om(U ), such that θ1(T ) = θ2(U ). Note the asymmetrical
role of T and U : a unifier for (T, U ) is not necessarily a unifier for (U, T ). The
notion of a most general unifier (mgu) is defined in the obvious way, see [
Triggers. Recall that for the classical chase a trigger for a tableau T is a pair (ξ, h), where ξ = α → β, and h(α) ⊆ T . Let us now return to example given in the beginning of this section. We had T = {R(a, b), R(X, c)}, and Σ = {ξ}, where ξ = {R(x, y), R(y, z) → S(x, z)}. We want to fire ξ on T resulting in conditional table ({R(a, b), R(X, c), S(a, c)}, ϕ), where ϕ(S(a, c)) is (X = b), and ϕ(t) remains true for the two other tuples t. We can fire ξ on T provided that we unify X with b. Formally, this is achieved by the trigger (ξ, ({x~a, y~b}, {X~b}, T ), where ({x~a, y~b}, {X~b}), is an mgu for the body of ξ, that is {R(x, y), R(y, z)}, and T . In general, the part of T that will be unified with the body of ξ is some subset of T . Let Σ be a set of tgd’s, and (T, ϕ) a conditional table. A trigger for Σ on (T, ϕ) is a tuple τ = (ξ, θ, T ′), where ξ ∈ Σ, and θ = (θ1, θ2) is an mgu that unifies the body of dependency ξ with T ′, where T ′ ⊆ T . The set t riggΣ(T, ϕ) contains the set of all triggers for Σ on (T, ϕ).
Example 1. Consider the conditional table (T, ϕ) with the following tabular representation:
t ϕ(t) R(X, b) true R(b, c) true
R(Y, d) true Let Σ = {ξ1, ξ2}, where tgd ξ1 is R(x, y), R(y, z) → S(x, z) and tgd ξ2 is S(x, x) → R(x, x). Then t riggΣ(T, ϕ) = {τ1, τ2, τ3, , τ4, τ5}, with τ1 = (ξ1, ({x~X, y~b, z~c}, {}), {R(X, b), R(b, c)}), τ2 = (ξ1, ({x~X, y~b, z~d}, {Y ~b}), {R(X, b), R(Y, d)}), τ3 = (ξ1, ({x~b, y~c, z~d}, {Y ~c}), {R(b, c), R(Y, d)}), τ4 = (ξ1, ({x~Y, y~d, z~b}, {X~d}), {R(Y, d), R(X, b)}), τ5 = (ξ1, ({x~c, y~c, z~b}, {X~c}), {R(b, c), R(X, b)}).
Note that ξ2, does not generate any triggers, as there are no tuples over relation name S. ◂
As applying a trigger on a c-table will generate new variables (unless the tgd is total), we need a mechanism for controlling this generation in such a way that the new variables are true representatives of the implicit Skolemization taking place. Let τ = (ξ, (θ1, θ2), T ′) be a trigger, where ξ = α(x, y) → ∃z β(x, z). For each z in z, consider a function z ↦ Zτ , such that if ρ = (ξ, (θ1, θ3), T ′′), then Zτ = Zρ. Clearly such a function exists (assuming Vars can be well ordered).
The following abbreviation will be useful. Let (T, ϕ) be a conditional table. Then we define ⩕(T, ϕ) =def
ϕ(t). t∈T Also, when θ is finite partial mapping from Vars to the set Vars ∪ Const we shall use the abbreviation ⩕(θ) =def
Xi = θ(Xi), i where the Xi’s are all the variables in the domain of θ. We are now ready to define the conditional chase step.
Let τ = (α → β, (θ1, θ2), T ′) ∈ t riggΣ(T, ϕ). We denote with θ1′ the extension of θ1 that maps each existentially quantified variable z from the tgd to the variable Zτ . We say that the conditional table (U, φ) is obtained from (T, ϕ) by applying the trigger τ if (U, φ) contains all the c-tuples from T together with their possibly modified local conditions, and possibly a new c-tuple, as follows: If T contains a tuple t that is syntactically equal to θ1′(β), then for (U, φ) the local condition of t is changed to where ⩕(τ ) denotes 2 the formula ⩕(T ′, ϕ) ∧ ⩕(θ2), else add the c-tuple θ1′(β) with local condition φ(t) =def ϕ(t) ∨ ⩕(τ ), φ(θ1′(β)) =def ⩕(τ ).
If (U, φ) is obtained from (T, ϕ) in this way we write (T, ϕ) →τ (U, φ), and call the transformation a conditional chase micro-step.
Having a table (T, ϕ) and a finite set Σ of tgd’s, the set of triggers t riggΣ (T, ϕ) is obviously finite. Consider a sequence
(T, ϕ) →τ1 (U1, ϕ1) →τ2 ⋯ →τn (Un, ϕn), where τ1, τ2, . . . , τn is an ordering of all the triggers from the set t riggΣ (T, ϕ). We call it a conditional chase micro-sequence for (T, ϕ) using t riggΣ (T, ϕ). Example 2. Let us continue with the c-table from Example 1. The c-table (U1, ψ1) in Figure 1 is obtained from (T, ϕ) in one chase micro-step by applying the trigger τ1. That is (T, ϕ) →τ1 (U1, ψ1). Next, by applying trigger τ2 to (U1, ψ1), we obtain (U2, ψ2). Note that the last tuple has a local condition generated by the substitution {Y ~b} from τ2. In the same way we apply τ3 to (U2, ψ2), obtaining (U3, ψ3). Then by applying τ4, c-table (U4, ψ4) is obtained, to which we apply τ5, obtaining c-table (U5, ψ5). This gives the following sequence of chase micro-steps:
(T, ϕ) →τ1 (U1, ψ1) →τ2 (U2, ψ2) →τ3 (U3, ψ3) →τ4 (U4, ψ4) →τ5 (U5, ψ5), where the c-tables in question are displayed in Figure 1.◂
We note that the order in which the triggers are applied in a conditional micro-sequence does affect the outcome, but we shall see that in the end the order will not matter.
After a micro-sequence, it is not guaranteed that the result will satisfy the dependencies. Then additional triggers will be generated. We therefore abstract a micro-sequence into a macro-step, as follows.
Let (T, ϕ) and (U, φ) be conditional tables, and Σ be a set of tgd’s. We write (T, ϕ) ⇒Σ (U, φ), if (U, φ) is obtained from (T, ϕ) by applying all micro-steps generated from t riggΣ (T, ϕ). The transformation from (T, ϕ) to (U, φ) is called a conditional chase macro-step using Σ. 2 Note that the formula ⩕(τ ) is uniquely determined by τ . Intuitively it represents the (“abducted”) conditions induced by τ and necessary for the body α to apply in the standard sense. (U1, ψ1) t ψ1(t) R(X, b) true R(b, c) true R(Y, d) true S(X, c) true (U2, ψ2) (U3, ψ3) (U4, ψ4) (U5, ψ5) t ψ2(t) t ψ3(t) t ψ4(t) t ψ5(t) R(X, b) true R(X, b) true R(X, b) true R(X, b) true R(b, c) true R(b, c) true R(b, c) true R(b, c) true R(Y, d) true R(Y, d) true R(Y, d) true R(Y, d) true S(X, c) true S(X, c) true S(X, c) true S(X, c) true S(X, d) Y = b S(X, d) Y = b S(X, d) Y = b S(X, d) Y = b
S(b, d) Y = c S(b, d) Y = c S(b, d) Y = c
S(Y, b) X = d S(Y, b) X = d
S(b, b) X = c
The macro-step is monotone, that is, if (T, ϕ) ⇒Σ (U, φ), then T ⊆ U and ϕ logically implies φ, which we by a slight abuse of notation denote ϕ ⊆ φ. We next introduce the concept of a conditional chase-sequence.
Let (T, ϕ) be a c-table and Σ a set of tgd’s. A sequence
(T0, ϕ0), (T1, ϕ1), . . . , (Tn, ϕn), . . . of c-tables, inductively constructed as (T0, ϕ0) = (T, ϕ), (Tω, ϕω) =
(Ti, ϕi), (Ti+1, ϕi+1) = (U, φ), where (Ti, ϕi) ⇒Σ (U, φ),
i∈ω is called a conditional chase sequence associated with (T, ϕ) and Σ. If there is an i ∈ ω, such that Rep(Ti, ϕi) = Rep(Ti+1, ϕi+1), we say that the conditional chase sequence terminates (in the finite).
Example 3. Continuing example 2, let (T0, ϕ0) = (T, ϕ) and (T1, ϕ1) = (U5, ψ5). Then (T0, ϕ0) ⇒Σ (T1, ϕ1). Next, t riggΣ(T1, ϕ1) = {τ1, τ2, τ3, τ4, τ5, τ6, τ7, τ8}, where τ1, . . . , τ5 are as before, and τ6 = (ξ2, ({x~d, y~d}, {X~d}), {S(X, d)}), τ7 = (ξ2, ({x~b, y~b}, {Y ~b}), {S(Y, b)}), τ8 = (ξ2, ({x~b, y~b}, {}), {S(b, b)}), By applying the triggers in the order τ1, τ2, . . . , τ8 we obtain another microsequence ending in (T2, ϕ2), shown in Figure 2. In other words, (T1, ϕ1) ⇒Σ (T2, ϕ2). Note that the conditional chase process is not finished yet, as for table (T2, ϕ2), beside the previous triggers the following new triggers need to be considered as well: τ9 = (ξ1, ({x~X, y~b, z~b}, {}), {R(X, b), R(b, b)}), τ10 = (ξ1, ({x~b, y~b, z~b}, {X~b}), {R(b, b), R(X, b)}), τ11 = (ξ1, ({x~Y, y~d, z~d}, {}), {R(Y, d), R(d, d)}), τ12 = (ξ1, ({x~d, y~d, z~d}, {Y ~d}), {R(d, d), R(Y, d)}).
(T2, ϕ2) t ϕ2(t) R(X, b) true R(b, c) true R(Y, d) true S(X, c) true S(X, d) Y = b ∨ Y = b S(b, d) Y = c ∨ Y = c S(Y, b) X = d ∨ X = d R(d, d) (Y = b ∨ Y = b) ∧ (X = d) R(b, b) ((X = d ∨ X = d) ∧ (Y = b)) ∨ (X = c) (T3, ϕ3) t ϕ3(t) R(X, b) true R(b, c) true R(Y, d) true S(X, c) true S(X, d) Y = b S(b, d) Y = c S(Y, b) X = d R(d, d) Y = b ∧ X = d R(b, b) (X = d ∧ Y = b) ∨ (X = c) S(X, b) (X = d ∧ Y = b) ∨ (X = c) S(Y, d) Y = b ∧ X = d By applying τ1, . . . , τ12 the micro-sequence will end up in the c-table (T3, ϕ3), in Figure 2. Thus (T0, ϕ0), (T1, ϕ1), (T2, ϕ2), (T3, ϕ3) is (the finite part of) a conditional chase sequence associated with (T, ϕ) and Σ. For readability, (T3, ϕ3) is shown in a “cleaner” isomorphically equivalent form.◂
The following result shows that no matter what order we choose to apply the triggers in the micro-sequences, the results of the corresponding conditional chase sequences are equivalent.
Theorem 1. Let (T, ϕ) be a conditional table and Σ a set of tgd’s. Then, let (T0, ϕ0), (T1, ϕ1), . . . , (Tn, ϕn), . . . and (T0′, ϕ′0), (T1′, ϕ′1), . . . , (Tn′ , ϕ′n), . . . be two distinct conditional chase sequences with different orders of triggers in their micro-sequences. Then Rep(Tω, ϕω) = Rep(Tω′ , ϕ′ω). Even more, Tω = Tω′ .
The theorem means that distinct orders in the micro-sequences only affect the syntactic form of the local conditions. The atoms in the table will be syntactically equal, and the corresponding local conditions equivalent.
We shall use the notation C hasecΣond(T, ϕ) for one representative of (Tω, ϕω) in the conditional chase sequence, starting with (T, ϕ) and Σ. We conclude this section by stating the main property of the conditional chase. The theorem means that the conditional chase computes exactly the set of constructible models. Theorem 2. Rep(C hasecΣond(T, ϕ)) = Σ(Rep(T, ϕ)). 4
We will show that the conditional chase with richly acyclic set of tgd’s always
terminates. The class of richly acyclic [
The oblivious chase. The oblivious chase proceeds as the standard chase,
except that each dependency is fired once for each trigger, irrespectively of whether
the trigger is active or not. As in the standard chase, we assume that all the
dependencies are applied fairly in the oblivious chase process. Fairness of the
oblivious chase means that each trigger, active or not, is eventually applied. The
details of how to construct a fair oblivious chase sequence are described in [
Enrichment of dependencies. In order to relate termination of the standard and the oblivious chase, we introduce a transformation, called enrichment, that takes a tuple generating dependency ξ = α(x, y) → ∃z β(x, z) and converts it into the tgd ξˆ = α(x, y) → ∃z β(x, z), H(x, y), where H is a new relational symbol that does not appear in R. For a set Σ of tgd’s, the transformed set is Σ̂ = {ξˆ ∶ ξ ∈ Σ}. We now have Theorem 3. C haseoΣbl(T ) terminates if and only if C hasesΣtand(T ) terminates. ̂ Proof. Let Σ be a set of tgd’s, and suppose that there is a tableau T for which the standard chase with Σ̂ does not terminate. This means that there is an infinite standard chase sequence
T = T0 ÐξˆÐ0, Ðh→′0 T1 ÐξˆÐ1, Ðh→′1 . . . . . . ÐξˆnÐ−Ð1, Ðh′nÐ−→1 Tn ÐξˆnÐ, Ðh→′n . . . .
Let αi denote the antecedent of ξˆi Then hi(αi) ⊆ Ti, for all i ∈ ω. Since αi also is the antecedent of ξi, we have that
T = U0 ÐξÐ0, Ðh→′0 U1 ÐξÐ1, Ðh→′1 . . . . . . ÐξnÐ−Ð1, Ðh′nÐ−→1 Un ÐξnÐ, Ðh→′n . . . , where Ui is Ti with all atoms over H deleted, is an infinite oblivious chase sequence with Σ on T .
Suppose then that there is a tableau T for which the oblivious chase with Σ does not terminate. Then there is an infinite oblivious chase sequence
T = T0 ÐξÐ0, Ðh→′0 T1 ÐξÐ1, Ðh→′1 . . . . . . ÐξnÐ−Ð1, Ðh′nÐ−→1 Tn ÐξnÐ, Ðh→′n . . . .
Let U0 = T0, and for all i ∈ ω, let
Ui+1 = Ti+1 ∪ {β(h′i(x), h′i(z)), H(h′i(x), h′i( y))}.
T = U0 ÐξˆÐ0, Ðh→′0 U1 ÐξˆÐ1, Ðh→′1 . . . . . . ÐξˆnÐ−Ð1, Ðh′nÐ−→1 Un ÐξˆnÐ, Ðh→′n . . . is an infinite standard chase sequence with Σ̂ on T . Suppose it is not. Then there must be an i ∈ ω, such that the standard chase step cannot be applied with hi and ξˆi on Ui. Let ξi = α(x, y) → β(x, z). Then ξˆi = α(x, y) → β(x, z), H(x, y). If ξˆi cannot be applied with hi on Ui, there exists an extension hie of hi such that β(hie(x), hie( z))) and H(hie(x), hie( y))) are in Ui. Since hie is an extension of hi, it follows that hie(x) = hi(x) and hie(y) = hi(y), meaning that H(hi(x), hi( y))) ∈ Ui. Because atoms over H are only introduced by the chase, it means that the homomorphism hi has already been applied with ξˆi earlier in the standard chase sequence. But then hi must also have been applied with ξi at the same earlier stage in the oblivious chase sequence. This is a contradiction, since it entails that ξi would have been fired twice with hi in the oblivious chase sequence.∎ Weakly and richly acyclic sets of tgd’s. For a set Σ of tgd’s over a database schema R the dependency graph of Σ is the directed graph that has as vertices (R, i), where R ∈ R, and i ∈ {1, . . . , arity(R)}. The graph has two types of edges: 1. Regular edges. There is a regular edge between vertices (R, i) and (S, j) if there a tgd in Σ that has a variable y that appears both in position (R, i) in the body, and in position (S, j) in the head. 2. Existential edges. There is an existential edge between vertices (R, i) and (S, j) if there is a tgd in Σ that has a variable y that appears in position (R, i) of the body and in some position in the head, and an existentially quantified variable z that appears in position (S, j) in the head.
A set of Σ of tgd’s is said to be weakly acyclic if the dependency graph of Σ
does not have any cycles containing an existential edge [
Hernich and Schweikardt [
Lemma 2. Let Σ be a richly acyclic set of tgd’s. Then Σ̂ is weakly acyclic.
Corollary 1. Let Σ be a richly acyclic set of tgd’s. Then C haseoΣbl(T ) terminates on all tableaux T .
It is easy to see that whenever the conditional chase terminates, the oblivious chase also terminates. The reverse is however not true.
Proposition 1. There exists a set Σ of tgd’s and a tableau T , such that the oblivious chase with Σ terminates on all instances (including T ), but the conditional chase with Σ does not terminate on (T, true).
Proof: Let Σ = {R(x, y, y) → ∃z, v R(x, z, v)}. Using the technique in [
t ϕ(t) R(a, b, b) true R(a, X1, X2) true R(a, X3, X4) X1 = X2 R(a, X5, X6) (X1 = X2) ∧ (X3 = X4) . . . . . .
In order to obtain the sufficient condition for the conditional chase termination we introduce our second rewriting of a set of tgd’s Σ, called disjoining, and denoted Σ¨ . Given a tgd ξ, we denote with ξ¨ the same dependency where for each variable x, that is repeated in the body, we replace all occurrences, except the first, of x in the body with a fresh new universally quantified variable. For instance, if ξ = R(x, y, x), R(y, z, x) → ∃v, w R(x, v, w), then ¨ ξ = R(x, y, x1), R(y1, z, x2) → ∃v, w R(x, v, w), where the subscripted variables are fresh. The set Σ¨ is then {ξ¨ ∶ ξ ∈ Σ}.
From the observation that a difference between the conditional and the oblivious chase is that the former may fire based on unifiers (θ1, θ2), and the latter based only on homomorphisms θ1, we obtain the following lemma. Lemma 3. C hasecΣond(T, ϕ) terminates if C haseoΣ¨bl(T ) terminates.
From the observation that the extended dependency graph for Σ¨ can be obtained from the extended dependency graph of Σ by deleting edges we get Lemma 4. If Σ is a richly acyclic set of tgd’s, then Σ¨ is also richly acyclic.
Theorem 4. Let Σ be a set of richly acyclic set of tgd’s and (T, ϕ) a c-table. Then C hasecΣond(T, ϕ) terminates.
Proof. By Lemma 4, the set Σ¨ is also richly acyclic, and by Lemma 2, the set
Σ̂¨ is weakly acyclic. By [
In this paper we have shown that the conditional chase with a richly acyclic set of dependencies terminates on all instances. This class is based on the well known weakly acyclic class of dependencies that ensures the standard chase termination on all instances. One may extend the class of dependencies for which the conditional chase terminates, by considering classes of dependencies for which the standard chase terminates (such as super weakly acyclic, safe constraints, Cstratified) and then using our characterization of the oblivious chase termination (Theorem 3) and by suitable extensions of Lemma 3.
Due to the space restrictions complexity results are not included. In the full version of this paper we show that for richly acyclic sets of dependencies the problem of checking if a tuple is the certain answer to a given first order query is coNP-complete and remains polynomial for unions of conjunctive queries.