Will My Favorite Chases Terminate if Evaluating Conjunctive Queries Does? One Does Not Simply Decide This
arXiv:2605.12349v1 [cs.DB] 12 May 2026
Lucas Larroque1 , Quentin Manière2 1 Inria, DI ENS, ENS, CNRS, PSL University, Paris, France 2 LIRMM, Inria, University of Montpellier, CNRS, Montpellier, France {lucas.larroque, quentin.maniere}@inria.fr Abstract Existential rules are a prominent formalism to enrich a database with knowledge from the domain of interest, but make even basic reasoning tasks on the resulting knowledge base undecidable. To circumvent this, several classes of rules offering various useful properties have been identified. One such class, for instance, contains all sets of rules on which the chase algorithm always terminates, which guarantees the existence of a finite universal model. However, these classes are often abstract rather than concrete: it may be undecidable to check whether a given set of rules belongs to them. Given that the most studied classes of existential rules are designed for reasoning on databases, thus ensuring decidable conjunctive query entailment, we ask: Within a class that supports decidable query entailment, do the usual abstract classes become concrete? We answer in the negative for classes based upon the termination of all classical chase variants and for the bts class.
1
Introduction
One of the main tasks in knowledge representation and reasoning is ontology-based data access (OBDA). In OBDA, an ontology is used to enrich a database with domain knowledge, enabling the inference of new information that is not explicitly stored in the database. Existential rules (also known as Datalog± , or tuplegenerating dependencies) are a prominent formalism to represent ontologies in OBDA [Fagin, 2018]. A fundamental reasoning task in OBDA is the Boolean conjunctive query (BCQ) entailment problem, which consists in deciding whether a BCQ is entailed by a database and an ontology of interest. Unfortunately, with ontologies expressed as sets of existential rules, BCQ entailment is undecidable in general [Beeri and Vardi, 1981; Calì et al., 2012]. To ensure decidable BCQ entailment, three main properties have been proposed. First, the chase procedure [Maier et al., 1979] is a materialization-based algorithm that, given a database and a set of existential rules, iteratively applies the rules
to the database to produce a (possibly infinite) universal model of the input. If finite, this universal model can then be queried using regular BCQ evaluation techniques to decide entailment. Many variants of the chase procedure exist, differing in the way rules are applied and redundancies are handled. In this paper, we consider the oblivious [Calì et al., 2013], semi-oblivious (a.k.a. Skolem) [Marnette, 2009], restricted (a.k.a. standard) [Fagin et al., 2005a], and core chase variants [Deutsch et al., 2008]. Guaranteed termination of the chase thus implies decidable BCQ entailment, but this property is also desirable in data exchange settings, where one is interested in translating data from a source schema to a target schema while preserving certain properties [Fagin et al., 2005b]. It also enables computing aggregates, which otherwise make little sense on infinite models [Afrati and Kolaitis, 2008], and ensures finite controllability, i.e. only considering finite models does not impact query answers. Second, query rewriting techniques aim at rewriting the input BCQ into a first-order query that can be directly evaluated over the input database. Rule sets for which such a rewriting exists (and is computable) are called fus, for finite unification set [Baget et al., 2009]. Again, fus rule sets have benefits beyond decidability of BCQ entailment, as they allow answering the rewritten query over any database. In particular, this allows answering queries even without edit access, or answering queries efficiently in streaming settings [Ronca et al., 2018]. Third, bounded treewidth sets (bts) [Calì et al., 2013] are classes of existential rules that ensure that, for any database, the universal model produced by the chase has bounded treewidth. This property renders BCQ entailment decidable by using Courcelle’s theorem [Courcelle, 1990], which states that any property definable in monadic second-order logic can be decided in linear time over structures of bounded treewidth. In particular, this helps with efficient answer counting [Feier et al., 2023]. Deciding whether a given set of existential rules has any of these properties (i.e. whether it guarantees termination of a certain chase variant, is fus, or is bts) is, here again, undecidable in general. The classes of such sets of rules are thus called abstract, as opposed to concrete classes for which membership is decidable. Efforts have been devoted to proving that, when restricting to some concrete classes
of existential rules, membership in the abstract classes presented above becomes decidable. This is especially the case for chase termination: oblivious and semi-oblivious chase termination have been proven decidable for guarded and for sticky rules [Calautti et al., 2015; Calautti and Pieris, 2019], while core chase termination is decidable for guarded rules [Hernich, 2012] but remains open for sticky rules. Restricted chase termination appears more difficult: its decidability has been proven for single-head guarded and sticky rules [Gogacz et al., 2020], but remains open in the multi-head case for both classes. The multi-head case for linear rules, a subclass of guarded rules, has been solved only recently [Gerlach et al., 2025]. These approaches vary greatly and often require sophisticated constructions, but they all share two properties: the considered concrete class always enjoys decidable BCQ entailment, and termination of the considered variant of the chase is always proved decidable. This raises the following question: do we get decidable chase termination (or fus membership? or bts membership?) for free when considering concrete classes of rules with decidable BCQ entailment? For fus, the answer is known to be negative, as shown by [Gaifman et al., 1993], who proved that boundedness of Datalog (which coincides with fus membership here) is undecidable. Surprisingly, for chase termination and bts membership, the question remains open. We answer it negatively in this paper: Theorem 1. There exists a concrete class 𝒞 of sets of existential rules such that: 1. Chase termination is undecidable in 𝒞 for the oblivious, semi-oblivious, restricted, and core chases, 2. 𝑏𝑡𝑠 membership is undecidable in 𝒞, and 3. BCQ entailment is decidable in 𝒞. This paper is dedicated to proving Theorem 1 by explicitly constructing such a class 𝒞, in Section 3, made of sets of rules that simulate Minsky machines. We then establish the negative results regarding chase termination and bts membership in Section 4, before proving decidability of BCQ entailment in Section 5. Our simulation of Minsky machines is inspired from [Gogacz and Marcinkowski, 2014], a paper interested in termination of the oblivious, semi-oblivious and restricted chases. We modify their construction in non-trivial ways to also support the core chase and to introduce a flooding mechanism that is instrumental in achieving the properties regarding bts membership and BCQ entailment.
2
Preliminaries
We mostly follow [Carral et al., 2022] for the preliminaries and assume some basic knowledge of first-order logic. First-Order Logic (FOL) We define Preds, Consts, and Vars to be mutually disjoint, countably infinite sets of predicates, constants, and variables, respectively. Every P ∈ Preds has an arity ar(P) ≥ 0. Let Terms = Consts ∪ Vars be the set of terms. We write lists 𝑡1 , . . . , 𝑡𝑛 of terms as 𝑡¯ and often treat them as sets. For a formula or set
thereof 𝜙, let Preds(𝜙), Consts(𝜙), Vars(𝜙), and Terms(𝜙) be the sets of all predicates, constants, variables, and terms that occur in 𝜙, respectively. A (P-)atom is a FOL formula P(𝑡¯) with P a |𝑡¯|-ary predicate and 𝑡¯ ∈ Terms. For a formula 𝜙, 𝜙[¯ 𝑥] indicates that 𝑥 ¯ contains all free variables that occur in 𝜙. Definition 2. An (existential) rule 𝑅 is a FOL formula (︀ )︀ ∀¯ 𝑥∀¯ 𝑦 𝐵[¯ 𝑥, 𝑦¯] → ∃¯ 𝑧 𝐻[¯ 𝑦 , 𝑧¯] (1) where 𝑥 ¯, 𝑦¯, and 𝑧¯ are pairwise disjoint lists of variables; and 𝐵 and 𝐻 are (finite) non-empty conjunctions of constant-free atoms, called the body and the head of 𝑅, respectively. The set 𝑦¯ is the frontier of 𝑅, denoted with fr(𝑅). If 𝑧¯ is empty, then 𝑅 is a Datalog rule. We usually omit universal quantifiers in rules. An instance ℐ is an existentially closed conjunction of atoms. Its active domain adom(ℐ) is the set of all terms occurring in ℐ. A Boolean conjunctive query (BCQ) has the same form as an instance, and we often identify both notions. A knowledge base (KB) 𝒦 is a tuple ⟨ℛ, ℐ⟩ with ℛ a rule set and ℐ an instance. We often identify rule bodies, rule heads, and instances with sets of atoms. Given atom sets ℐ and ℐ ′ , a homomorphism ℎ from ℐ to ′ ℐ is a function with domain Vars(ℐ) such that ℎ(ℐ) ⊆ ℐ ′ ; ℎ is an isomorphism from ℐ to ℐ ′ if additionally, ℎ is injective and ℎ−1 is a homomorphism from ℐ to ℐ ′ . A homomorphism ℎ from ℐ to ℐ ′ is a retraction if ℎ is the identity over Vars(ℐ) ∩ Vars(ℐ ′ ). We identify logical interpretations with atom sets. An atom set ℐ satisfies a rule 𝑅 = 𝐵 → ∃¯ 𝑧 𝐻 if, for every ^ homomorphism ℎ from 𝐵 to ℐ, there is an extension ℎ ^ of ℎ with ℎ(𝐻) ⊆ ℐ; equivalently, ℐ is a model of 𝑅. An atom set ℳ is a model of an instance ℐ if there is a homomorphism from ℐ to ℳ, and it is a model of a KB ⟨ℛ, ℐ⟩ if it is a model of ℐ and satisfies all rules in ℛ. Given KBs or atom sets 𝐴 and 𝐵, 𝐴 entails 𝐵, written 𝐴 |= 𝐵, if every model of 𝐴 is a model of 𝐵; 𝐴 and 𝐵 are equivalent if 𝐴 |= 𝐵 and 𝐵 |= 𝐴. Given atom sets ℐ and ℐ ′ , it is known that ℐ |= ℐ ′ iff there is a homomorphism from ℐ ′ to ℐ. A model ℳ of a KB 𝒦 is universal if there is a homomorphism from ℳ to every model of 𝒦. Every KB 𝒦 admits some (possibly infinite) universal model [Deutsch et al., 2008]. Hence, 𝒦 |= 𝑞 for any BCQ 𝑞 iff there is a homomorphism from a universal model of 𝒦 to 𝑞. The BCQ entailment problem takes as input a KB 𝒦 and a BCQ 𝑞 and asks if 𝒦 |= 𝑞; it is undecidable [Beeri and Vardi, 1981]. The chase The chase is a family of procedures that repeatedly apply rules until a fixpoint is reached. Definition 3 (Triggers and derivations). Given an instance ℐ, a trigger 𝑡 on ℐ is a tuple ⟨𝑅, 𝜋⟩ with 𝑅 = 𝐵 → ∃¯ 𝑧 𝐻 a rule and 𝜋 a homomorphism from 𝐵 to ℐ. Let supp(𝑡) = 𝜋(𝐵) and out(𝑡) = 𝜋 𝑅 (𝐻), where 𝜋 𝑅 extends 𝜋 by mapping all 𝑧 ∈ 𝑧¯ to the fresh variable 𝑧𝑡 that is unique for 𝑧 and 𝑡. A derivation from a KB ⟨ℛ, ℐ⟩ is a sequence 𝒟 = (∅, ℐ0 ), (𝑡1 , ℐ1 ), . . . such that: 1. Every ℐ𝑖 in 𝒟 is an instance; moreover, ℐ0 = ℐ.
2. Every 𝑡𝑖 in 𝒟 is a trigger ⟨𝑅, 𝜋⟩ on ℐ𝑖−1 such that 𝑅 ∈ ℛ, out(𝑡𝑖 ) ̸⊆ ℐ𝑖−1 , and ℐ𝑖 = ℐ𝑖−1 ∪ out(𝑡𝑖 ). The result res(𝒟) of 𝒟 is the union of all instances in 𝒟, and trigs(𝒟) is the set of all triggers in 𝒟. Different chase variants build specific derivations according to different criteria of trigger applicability. Below, the letters O, SO, R, and E respectively refer to the oblivious, semi-oblivious, restricted, and equivalent1 variants. Definition 4 (Applicability). A trigger 𝑡 = ⟨𝑅, ℎ⟩ on an instance ℐ is O-applicable on ℐ if out(𝑡) ̸⊆ ℐ; SOapplicable on ℐ if out(𝑡′ ) ̸⊆ ℐ for every trigger 𝑡′ = (𝑅, 𝜋 ′ ) with 𝜋(fr(𝑅)) = 𝜋 ′ (fr(𝑅)); R-applicable on ℐ if there is no retraction from ℐ ∪ out(𝑡) to ℐ; E-applicable on ℐ if there is no homomorphism from ℐ ∪ out(𝑡) to ℐ. Example 1. Consider the KB 𝒦 = ⟨ℛ, ℐ⟩ with ℛ = {𝑅 = P(𝑥, 𝑦) → ∃𝑧 P(𝑦, 𝑧), P(𝑧, 𝑧)} and ℐ = {P(𝑎, 𝑎)} for some 𝑎. The trigger 𝑡1 = (𝑅, {𝑥 ↦→ 𝑎, 𝑦 ↦→ 𝑎}), whose output is out(𝑡1 ) = {P(𝑎, 𝑧𝑡1 ), P(𝑧𝑡1 , 𝑧𝑡1 )}, is O and SOapplicable on ℐ but not R or E-applicable, since there is a retraction from ℐ ∪ out(𝑡1 ) to ℐ that maps 𝑧𝑡1 to 𝑎. Definition 5 (X-Chase). For an X ∈ {O, SO, R, E}, an X-derivation from a KB 𝒦 = ⟨ℛ, ℐ⟩ is a derivation 𝒟 such that every trigger 𝑡𝑖 ∈ trigs(𝒟) is X-applicable on ℐ𝑖 . An X-derivation 𝒟 is fair if for every ℐ𝑖 occurring in 𝒟 and X-applicable trigger 𝑡 on ℐ𝑖 , there is some 𝑗 > 𝑖 such that 𝑡 is not X-applicable on ℐ𝑗 . An X-derivation is terminating if it is fair and finite. The result of any fair X-derivation is a universal model of the KB, for X ∈ {O, SO, R}, and has a retraction to a universal model for X = E. Therefore, we obtain: Proposition 6. Consider a BCQ 𝑞, a KB 𝒦, and some fair X-derivation 𝒟 from 𝒦 where X ∈ {O, SO, R, E}. Then, 𝒦 |= 𝑞 iff res(𝒟) |= 𝑞. These chase variants induce abstract classes, whose relationship is summarized in [Carral et al., 2022]. Definition 7 (Chase-Terminating Sets). For an X ∈ X {O, SO, R, E}, let CTX ∀ (resp. CT∃ ) be the set of all rule sets ℛ such that every (resp. some) fair X-derivation from every KB ⟨ℛ, ℐ⟩ is finite. X Proposition 8. For all X ∈ {O, SO, E}, CTX ∀ = CT∃ , O SO R R E and CT∀ ⊂ CT∀ ⊂ CT∀ ⊂ CT∃ ⊂ CT∀ . Example 2. Consider the KB 𝒦 = ⟨ℛ, ℐ⟩ from Example 1. All fair O- or SO-derivations from 𝒦 are infinite. The only fair R and E-derivation from 𝒦 is 𝒟 = (∅, ℐ). Any fair R-derivation from a KB with ℛ is finite and E hence, ℛ ∈ CTR ∀ (and thus ℛ ∈ CT∀ ). bts The class bts is defined from the notion of treewidth and contains CTX 𝑄 for all X ∈ {O, SO, R, E} and 𝑄 ∈ {∃, ∀} [Calì et al., 2013]. We only introduce a sufficient condition for a rule set not to be bts. Given a binary predicate P, the P-graph of an instance ℐ is the directed graph (adom(ℐ), 𝐸) where (𝑎, 𝑏) ∈ 𝐸 if and only if P(𝑎, 𝑏) ∈ ℐ. 1
The equivalent chase, like the better-known core chase, halts exactly when the KB has a finite universal model [Delivorias et al., 2021], while being monotonic (∀𝑖, ℐ𝑖 ⊆ ℐ𝑖+1 ).
Proposition 9. If there is an infinite clique in the Pgraph of res(𝒟) for some binary predicate P and derivation 𝒟 from 𝒦 = ⟨ℐ, ℛ⟩, then ℛ is not bts.
2.1
Three-counter Machines
A three-counter machine (3CM) ℳ is essentially a twocounter automaton augmented with a strictly increasing time counter. Formally, it is a tuple ⟨𝑄, 𝑞1 , 𝛿⟩ where 𝑄 is a finite set of states including the initial state 𝑞1 , and 𝛿 : 𝑄 × {0, 1}2 → 𝑄 × {−1, 0, 1}2 is a transition function. A configuration of ℳ is a tuple ⟨𝑞, 𝑣1 , 𝑣2 , 𝑡⟩ where 𝑞 ∈ 𝑄 is the current state and 𝑣1 , 𝑣2 , 𝑡 ∈ N are the values of the three counters. The initial configuration of ℳ is ⟨𝑞1 , 0, 0, 0⟩. Given a configuration 𝐶 = ⟨𝑞, 𝑣1 , 𝑣2 , 𝑡⟩, we define next(𝐶) = ⟨𝑞 ′ , 𝑣1′ , 𝑣2′ , 𝑡 + 1⟩ where 𝛿(𝑞, 𝑏1 , 𝑏2 ) = ⟨𝑞 ′ , 𝑑1 , 𝑑2 ⟩ where 𝑏𝑖 = 0 if 𝑣𝑖 = 0 and 𝑏𝑖 = 1 otherwise, and 𝑣𝑖′ = max(𝑣𝑖 + 𝑑𝑖 , 0) for 𝑖 ∈ {1, 2}. Note that next is a partial function since 𝛿 may be undefined for some inputs. A 3CM ℳ halts if there is a finite sequence of configurations 𝐶0 , . . . , 𝐶𝑛 such that 𝐶0 is the initial configuration, 𝐶𝑖+1 = next(𝐶𝑖 ) for every 0 ≤ 𝑖 < 𝑛, and next(𝐶𝑛 ) is undefined. The halting problem for 3CMs is undecidable [Minsky, 1967].
3
The Rule Set
We define the class 𝒞 = { ℛℳ | ℳ a 3CM }, using the rule set ℛℳ given in Figure 1. As it is recognizable in linear time, it is indeed a concrete class. The rule set ℛℳ is a adapted from the one used to prove Theorem 1 in [Gogacz and Marcinkowski, 2014], stating that allinstance chase termination is undecidable for the oblivious chase. It provides a reduction from the halting problem for 3CMs to chase termination. Roughly speaking, the chase on KB ⟨{End(𝑤)}, ℛℳ ⟩ looks like a sequence of elements connected through a binary predicate S, ending in the “well of positivity” 𝑤. Each element in the chase runs its own private computation of ℳ, and is only allowed to generate a predecessor if the simulation of ℳ goes on for long enough. Consequently, this chain of elements is infinite if and only if ℳ does not halt. To elaborate, we first need to explain how ℳ can be simulated by a sequence of natural numbers. Following Section 3.3 in [Gogacz and Marcinkowski, 2014], there is a way to encode configurations of a 3CM ℳ as natural numbers using prime factorization. Let 𝑝1 , 𝑝2 , . . . be the sequence of prime numbers, and 𝑄 = {𝑞1 , . . . , 𝑞𝑚 }. Then, a configuration ⟨𝑞𝑖 , 𝑣1 , 𝑣2 , 𝑡⟩ of ℳ is encoded as the natural number 1 2 enc(𝑞𝑖 , 𝑣1 , 𝑣2 , 𝑡) = 𝑝𝑖 · 𝑝𝑣𝑚+1 · 𝑝𝑣𝑚+2 · 𝑝𝑡𝑚+3 .
In particular, the initial configuration ⟨𝑞1 , 0, 0, 0⟩ is encoded as 2 = 𝑝1 . Let 𝑝 = 𝑝1 . . . 𝑝𝑚+3 . Proposition 10. There exist natural numbers 𝑞𝑖 , 𝑟𝑖 for all 1 ≤ 𝑖 ≤ 𝑝 such that 𝑟𝑞𝑖𝑖 is irreducible, and for any configuration 𝐶 of ℳ such that 𝑖 = enc(𝐶) mod 𝑝, if next(𝐶) is defined, then enc(next(𝐶)) = 𝑟𝑞𝑖𝑖 · enc(𝐶), and 𝑞𝑖 𝑟𝑖 · enc(𝐶) = enc(𝐶) otherwise.
S0 (𝑥, 𝑦) → S(𝑥, 𝑦) R𝑖 (𝑥, 𝑦), S(𝑦, 𝑧) → R𝑖+1 (𝑥, 𝑧) 𝑟𝑖
′
𝑞𝑖
′
′
′
T𝑖 (𝑥, 𝑦, 𝑧), S (𝑦, 𝑦 ), S (𝑧, 𝑧 ) → T𝑖 (𝑥, 𝑦 , 𝑧 ) S(𝑥, 𝑦) → Flood(𝑦)
(𝑅S ) (𝑅R,𝑖 ) (𝑅T,𝑖 ) prop (𝑅flood )
End(𝑥) → S(𝑥, 𝑥)
(𝑅SEnd )
2
S (𝑥, 𝑦) → G(𝑥, 𝑦)
(𝑅Ginit )
G(𝑥, 𝑦), R𝑖 (𝑥, 𝑦), T𝑖 (𝑥, 𝑦, 𝑧) → G(𝑥, 𝑧)
step (𝑅G,𝑖 )
Flood(𝑥), Flood(𝑦), Flood(𝑧) → G(𝑥, 𝑦),
𝑝−1 ⋀︁
R𝑗 (𝑥, 𝑦), T𝑗 (𝑥, 𝑦, 𝑧)
𝑗=0 𝑝−1 ⋀︁
G(𝑦, 𝑧), End(𝑧) → ∃𝑥 S0 (𝑥, 𝑦), R0 (𝑥, 𝑥),
T𝑗 (𝑥, 𝑥, 𝑥)
gen (𝑅flood )
(𝑅∃ )
𝑗=0
Figure 1: Rules in ℛℳ for all 𝑖 < 𝑝. In Rule 𝑅R,𝑖 , R𝑝 is interpreted as R0 . S𝑛 (𝑥, 𝑦) denotes an S-path of length 𝑛 from 𝑥 to 𝑦.
For further details, we refer the reader to Theorem 5 in [Gogacz and Marcinkowski, 2014]. Let 𝑔 be the func𝑞 𝑝 tion defined as 𝑔(𝑛) = 𝑟𝑛𝑛 mod · 𝑛. Then, next(𝐶) is mod 𝑝 defined if and only if 𝑔(enc(𝐶)) ̸= enc(𝐶), and in that case enc(next(𝐶)) = 𝑔(enc(𝐶)). Let 𝒢 = { 𝑔 𝑖 (2) | 𝑖 ∈ N }. Since the third counter always increases when a subsequent configuration exists, we get the following. Proposition 11. ℳ halts iff 𝒢 is bounded. Then, as mentioned earlier, the chase is shaped as a sequence of elements that form a chain connected by predicates S, where S(𝑥, 𝑦) means that 𝑦 thinks it is the successor of 𝑥. The use of “thinks” is intentional, as we run a simulation of ℳ from the point of view of each element. All predicates used for the simulation (G, R𝑖 and T𝑖 ) feature this element in first position, which thinks itself as 0. The atom G(𝑥, 𝑦) signifies that from the point of view of 𝑥, the number represented by 𝑦 belongs to 𝒢. This relation is computed according to Proposition 10, step using Rules 𝑅Ginit and 𝑅G,𝑖 . Specifically, the initial configuration is encoded by 2, represented by the second step successor of each element (Rule 𝑅Ginit ). Rule 𝑅G,𝑖 then implements the transition to the next configuration using predicates R𝑖 and T𝑖 . The atom R𝑖 (𝑥, 𝑦) indicates that, from 𝑥’s perspective, the number represented by 𝑦 has a remainder of 𝑖 modulo 𝑝, as generated by Rule 𝑅R,𝑖 . Similarly, T𝑖 (𝑥, 𝑦, 𝑧) implies that 𝑦𝑧 = 𝑟𝑞𝑖𝑖 from 𝑥’s perspective. This is ensured by Rule 𝑅T,𝑖 , which implements multiplication by successive additions. These predicates are initialized for each element 𝑥 by Rule 𝑅∃ . This rule allows an element 𝑦 to create a predecessor 𝑥 (specifically S0 (𝑥, 𝑦), which implies S(𝑥, 𝑦) via Rule 𝑅S ) if the simulation of ℳ from 𝑦 reaches the well of positivity 𝑤 (i.e., when G(𝑦, 𝑧) and End(𝑧) hold for some 𝑧). This process is illustrated in Figure 2 for predicate T𝑖 . The reduction described so far mirrors the one in [Gogacz and Marcinkowski, 2014]. However, the same reduction does not work here. First, it applies only to the oblivious chase; the restricted and equivalent chases always terminate, even if ℳ does not halt. Second, arguing that BCQ entailment is decidable is difficult (and likely false) because the predicates R𝑖 , T𝑖 , and G lack structure. We introduce two modifications to address these issues. First, to accommodate all chase variants, we introduce
predicates S0 and End, which derive S via Rules 𝑅S and 𝑅SEnd . In particular, S0 has no self-loop over the well of positivity 𝑤 (where End(𝑤) holds, at the end of the chain), preventing any attempt at homomorphically embedding the whole chain into 𝑤. Thus, even the equivalent chase is forced to create an infinite chain if ℳ does not halt. Second, to make BCQ entailment decidable, we employ a flooding mechanism using the predicate Flood, gen prop with Rules 𝑅flood and 𝑅flood . This ensures that once the simulation from 𝑥 reaches 𝑤 and generates a predecessor, 𝑥 connects to all its successors via R𝑖 , T𝑖 , and G. As a result, all elements whose simulation reaches the well of positivity show the same behavior regarding BCQ answering, except for predicates S0 , S and End which are easier to handle.
4
Undecidability of Chase Termination and bts-Recognition
This section is devoted to Points 1 and 2 of Theorem 1, which are the negative properties of our class: chase termination for all chase variants and bts are both undecidable in 𝒞. Regarding Oblivious and Semi-Oblivious chase termination, this is mostly guaranteed by construction, as we adapted the class proposed in [Gogacz and Marcinkowski, 2014] that already had these properties. Remarkably, our set of rules also exhibits this behavior for the equivalent chase. To prove this, we make use of Proposition 8 as much as possible. More precisely, we show that if ℳ does not halt, then the equivalent chase does not terminate on ℛℳ and some specific instance ℐE (Theorem 14), and that if ℳ does halt, then the oblivious chase terminates on the so-called critical instance, and thus on all instances (Theorem 16). These two results, along with Proposition 8 and the undecidability of the halting problem for 3CMs entail that chase termination is undecidable for 𝒞. The undecidable bts recognition is then a consequence of the above, joint with our freshly added flooding mechanism. In this section, X always denotes an element of {O, SO, R, E}. We denote the result of some fair Xderivation from ℐ, ℛ with ChX (ℐ, ℛ). Note that this object is not unique in general, as different derivations may produce different results. This is however not an
Step 3
Step 1
T𝑖
T𝑖
Step 0
𝑡0
S
𝑡1
S
𝑡2
𝑡3
S
S
𝑡4
S
T𝑖 T𝑖
Step 2
𝑤
S End
Figure 2: Representation of predicates S0 , End and atoms with shape T𝑖 (𝑡0 , _, _) in ChX5 (ℐE ) for some 𝑖 such that 𝑟𝑞𝑖𝑖 = 23 . The S0 -atoms, as described in Lemma 12, form a chain ending in 𝑤, the only term with End(𝑤). Then, T𝑖 -atoms are as described by Lemma 13: First, T𝑖 (𝑡0 , 𝑡0 , 𝑡0 ) is created by the application of Rule (𝑅∃ ) that creates 𝑡0 (step 0). Then, T𝑖 (𝑡0 , 𝑡2 , 𝑡3 ), T𝑖 (𝑡0 , 𝑡4 , 𝑡6 ), and T𝑖 (𝑡0 , 𝑡6 , 𝑡9 ) (note that 𝑤 = 𝑡6 = 𝑡9 ) are created by successive applications of Rule (𝑅T,𝑖 ) (steps 1, 2 and 3, respectively).
issue for our purpose, since we do not really consider the restricted chase in proofs, and it is the only variant for which the order of application of triggers matters. It will also be convenient to consider the chase as an alternation of closing under Datalog rules and then under X ∀ non-Datalog rules. We define ChX 0 (ℐ) = Ch (ℐ, ℛℳ ) and X X X X ∃ for all 𝑖 ≥ 0, Ch𝑖+1 (ℐ) = Ch (Ch (Ch𝑖 (ℐ), ℛℳ ), ℛ∀ℳ ), where ℛ∀ and ℛ∃ denote the sets of Datalog and nonDatalog rules in ℛ, respectively. Note that this process still induces a fair derivation.
4.1
Non-Termination of the Chase
We first prove that if ℳ does not halt, then ℛℳ ∈ / CTX 𝑄 for 𝑄 ∈ {∀, ∃}, by considering only the instance ℐE = {End(𝑤)}. Before proving this, we need two lemmas about the structure of the chase. X Lemma 12. For all 𝑛 > 0, if ChX 𝑛 (ℐE ) ̸= Ch𝑛−1 (ℐE ), then adom(ChX 𝑛 (ℐE )) = {𝑡0 , . . . , 𝑡𝑛−1 , 𝑤} for some terms 𝑡0 , . . . , 𝑡𝑛−1 , and the S0 -atoms of ChX 𝑛 (ℐE ) are exactly { S0 (𝑡𝑖 , 𝑡𝑖+1 ) | 0 ≤ 𝑖 < 𝑛 } where 𝑡𝑛 = 𝑤.
Proof sketch. By induction on 𝑛. Both the base case and inductive step follow from the fact that there is a single existential rule, and thus the only way for ChX 𝑛 (ℐE ) to be different from ChX 𝑛−1 (ℐE ) is for Rule 𝑅∃ to be applied. This rule features a single frontier variable, which has to be mapped to the term created at the previous step. In the following lemma, proven by a simple induction, we refer to terms of ChX 𝑛 (ℐE ) as 𝑡0 , . . . , 𝑡𝑛−1 as in Lemma 12. We also use 𝑡𝑖 for 𝑖 ≥ 𝑛 to refer to 𝑤. Note that even for such 𝑖’s, S(𝑡𝑖 , 𝑡𝑖+1 ) ∈ ChX 𝑛 (ℐE ). X Lemma 13. For all 𝑛 > 0, if ChX 𝑛 (ℐE ) ̸= Ch𝑛−1 (ℐE ),
(i) R𝑖 (𝑡0 , 𝑡𝑘 ) ∈ ChX 𝑛 (ℐE ) if and only if 𝑘 = 𝑖 mod 𝑝; (ii) T𝑖 (𝑡0 , 𝑡𝑘 , 𝑡𝑙 ) ∈ ChX 𝑛 (ℐE ) if and only if there is 𝑚 such that 𝑘 = 𝑚𝑟𝑖 and 𝑙 = 𝑚𝑞𝑖 ; (iii) For all 𝑘 ∈ N, G(𝑡0 , 𝑡𝑔𝑘 (2) ) ∈ ChX 𝑛 (ℐE ); (iv) If 𝒢 is bounded by 𝑛 − 1, then for all 𝑙 such that 𝑘 G(𝑡0 , 𝑡𝑙 ) ∈ ChX 𝑛 (ℐE ), there is 𝑘 such that 𝑙 = 𝑔 (2).
Theorem 14. If ℳ does not halt, there is no terminating X-chase sequence from ⟨{End(𝑤)}, ℛℳ ⟩. Proof sketch. We simply prove by induction on 𝑛 that if X ℳ does not halt and ChX 𝑛 (ℐE ) ̸= Ch𝑛−1 (ℐE ), then Rule 𝑅∃ X is E-applicable on Ch𝑛 (ℐE ). In this case, ChX 𝑛 (ℐE ) is as described in Lemma 12. Then, by Proposition 11, 𝒢 is unbounded, so G(𝑡0 , 𝑤) ∈ ChX 𝑛 (ℐE ) by Item (iv) of Lemma 13. As the S0 -atoms of ChX 𝑛 (ℐE ) are exactly { S0 (𝑡𝑖 , 𝑡𝑖+1 ) | 0 ≤ 𝑖 < 𝑛 }, there is no way to homomorphically map the result of applying 𝑅∃ into ChX 𝑛 (ℐE ), so this rule is indeed E-applicable.
4.2
Termination of the Chase
To prove that the X-chase terminates if ℳ halts (Theorem 16), it suffices to prove that in this case, the oblivious chase terminates on the so-called critical instance. The critical instance is the instance containing a single constant 𝑤, and in which all possible facts over the schema of the rule set are present. Indeed, if the oblivious chase terminates on the critical instance, it terminates on all instances [Marnette, 2009], and thus all chase variants terminate too via Proposition 8. Let 𝒥 be the critical instance for the schema of ℛℳ , and 𝒥𝑛 = ChX 𝑛 (𝒥). Lemma 15. For all 𝑛 ∈ N, 𝒥𝑛 ≃ ChO 𝑛 (ℐE ) ∪ {S0 (𝑤, 𝑤)}. Proof sketch. By induction on 𝑛. The base case is obprop gen tained using Rules 𝑅SEnd , 𝑅flood and 𝑅flood . For the inductive step, the additional S0 -atom of 𝒥𝑛 can only produce S(𝑤, 𝑤), which already belongs to 𝒥. Thus, both instances feature the same applicable triggers. Theorem 16. If ℳ halts, then the X-chase terminates on ⟨ℐ, ℛℳ ⟩ for all instances ℐ. Proof sketch. If ℳ halts, then 𝒢 is bounded by 𝑛 and by Items (iii) and (iv) of Lemma 13, G(𝑡0 , 𝑤) ∈ / 𝒥𝑛+1 . Thus, Rule 𝑅∃ is not applicable on 𝒥𝑛+1 , which entails the result as discussed before Lemma 15.
4.3
Treewidth
We then prove that bts-membership in 𝒞 is undecidable. Theorem 17. ℛℳ is bts if and only if ℳ halts. If ℳ halts, then by Theorem 16, the X-chase terminates, so the rule set is clearly bts. The converse direction is a direct consequence of the flooding mechanism. Lemma 18. If ℳ does not halt, then there is an infinite clique in the R0 -graph of ChX ({End(𝑤)}, ℛℳ ). Proof. Assume ℳ does not halt. By Theorem 14, X for all 𝑛, ChX 𝑛 (ℐE ) ̸= Ch𝑛−1 (ℐE ), so by Lemma 12, there is an infinite sequence of terms 𝑢0 , 𝑢1 , . . . such that 𝑢0 = 𝑤, and for all 𝑖 ≥ 0, S(𝑢𝑖+1 , 𝑢𝑖 ) ∈ prop ChX ({End(𝑤)}, ℛℳ ). By Rule 𝑅flood , for all 𝑖, 𝑗 ≥ 0, gen X Flood(𝑢𝑖 ) ∈ Ch ({End(𝑤)}, ℛℳ ), so by Rule 𝑅flood , R0 (𝑢𝑖 , 𝑢𝑗 ) is also in the chase result, so the R0 -graph contains an infinite clique. Lemma 18 and Proposition 9 conclude the proof.
5
Decidability of BCQ Entailment
We now turn to decidability of BCQ entailment, that is Point 3 of Theorem 1. Consider an instance ℐ, a set of rules ℛℳ from our class 𝒞 constructed in Section 3, and a BCQ 𝑞. To decide whether ⟨ℐ, ℛℳ ⟩ |= 𝑞, our algorithm computes the result of the semi-oblivious chase up to depth 𝑀 := 2 |𝑞| + 1, that is ChSO 𝑀 (ℐ), and then checks whether ChSO (ℐ) |= 𝑞. This clearly terminates as we only 𝑀 require to apply finitely many rules in the first step, and then evaluate a usual BCQ on a finite instance in the second step. It remains to prove the correctness: Lemma 19. ⟨ℐ, ℛℳ ⟩ |= 𝑞 iff ChSO 𝑀 (ℐ) |= 𝑞. The rest of this section is devoted to proving the above. ⋃︀We first define ℐ𝑛 := ChSO 𝑛 (ℐ) for all 𝑛, and ℐ∞ := 𝑛≥0 ℐ𝑛 . The successive ℐ𝑛 again induce a fair derivation, therefore ℐ∞ is a universal model of ⟨ℐ, ℛℳ ⟩. Thus, Lemma 19 can be rephrased as ℐ∞ |= 𝑞 iff ℐ𝑀 |= 𝑞 using Proposition 6. With this formulation, the ‘if’ direction is the easiest one: indeed, if ℐ𝑀 |= 𝑞, we get ℐ∞ |= 𝑞 from the fact that ℐ∞ contains ℐ𝑀 . We now turn to proving the ‘only-if’ direction of Lemma 19. Assume ℐ∞ |= 𝑞. Compactness guarantees that there exists 𝑁 such that ℐ𝑁 |= 𝑞. If 𝑁 ≤ 𝑀 , we are done since ℐ𝑁 ⊆ ℐ𝑀 . Otherwise, if 𝑁 > 𝑀 , consider a homomorphism ℎ from 𝑞 to ℐ𝑁 . We want to construct a homomorphism ℎ′ : 𝑞 → ℐ𝑀 based on ℎ. Our main issue is atoms that ℎ maps to ℐ𝑁 ∖ ℐ𝑀 , for which we need to find replacements within ℐ𝑀 . Intuitively, we distinguish between the End-atoms (which cannot be introduced during the chase), the S0 atoms, the S-atoms, and the others. Indeed, apart from within the original instance ℐ, the S0 - and S-atoms form chains ending on some element from adom(ℐ). Therefore, if ℎ involves such S0 - and S-atoms from ℐ𝑁 ∖ ℐ𝑀 , we know they lie along a chain, say at distance ℓ to ℐ. We can then prove that a sufficient part of this chain already
belongs to ℐ𝑀 , due to 𝑀 ≥ 2 |𝑞|. To build ℎ′ , we can thus ‘shift’ ℎ by ℓ − 𝑀 atoms to use instead this part of the chain. Furthermore, we can establish that every term from ℐ𝑁 lies on such a chain, therefore, when we shift our homomorphism along the chain, due to the combination prop gen of Rules 𝑅flood and 𝑅flood , all the P-atoms are present for P ∈ / {End, S0 , S}. The only exception is when such a P-atom features a term 𝑡 that is the starting point of a prop chain (thus Rule 𝑅flood may not trigger on 𝑡) and that ℓ ≤ 𝑀 (so that we don’t shift). But ℓ ≤ 𝑀 guarantees the atom already belongs to ℐ𝑀 . We summarize considerations on S0 - and S-atoms in the next lemma, whose proof is a simple induction: Lemma 20. For all 𝑛 ≥ 0 and 𝑎 ∈ adom(ℐ), there exist integers 0 ≤ 𝑚𝑎 ≤ 𝑛 s.t.: (i) the domain of ℐ𝑛 consists of distinct terms 𝑎𝑖 with 𝑎 ∈ adom(ℐ) and 0 ≤ 𝑖 ≤ 𝑚𝑎 , and where 𝑎0 = 𝑎; and (ii) S0 atoms of ℐ𝑛 are exactly: {S0 (𝑎, 𝑏) | S0 (𝑎, 𝑏) ∈ ℐ} ∪ {S0 (𝑎𝑖+1 , 𝑎𝑖 ) | 0 ≤ 𝑖 < 𝑚𝑎 , 𝑎 ∈ adom(ℐ)}, and, as a corollary, the S atoms of ℐ𝑛 are exactly: {S(𝑎, 𝑏) | S(𝑎, 𝑏) ∈ ℐ or S0 (𝑎, 𝑏) ∈ ℐ} ∪ {S(𝑎, 𝑎) | End(𝑎) ∈ ℐ} ∪ {S(𝑎𝑖+1 , 𝑎𝑖 ) | 0 ≤ 𝑖 < 𝑚𝑎 , 𝑎 ∈ adom(ℐ)}. Note that the above echoes Lemma 12, except that the end point can now be any element from the original instance ℐ. Notice that using the semi-oblivious chase also prevents branching: each element from adom(ℐ) can only be the end point of one such chain of fresh elements. The result of the chase is depicted in Figure 3. We now clarify that, as the chase progresses, new facts either stem from the flooding mechanism or involve one of the freshly introduced starting points of a chain. Lemma 21. Let 𝑛 ≥ 0 and P(𝑡1 , . . . , 𝑡𝑚 ) an atom. If P(𝑡1 , . . . , 𝑡𝑚 ) ∈ ℐ𝑛+1 ∖ ℐ𝑛 then one of the following holds: 1. 𝑡1 ∈ adom(ℐ𝑛+1 ) ∖ adom(ℐ𝑛 ) and there are 𝑘2 ,. . . , 𝑘𝑚 ≥ 0 s.t. S𝑘2 (𝑡1 , 𝑡2 ), . . . , S𝑘𝑚 (𝑡1 , 𝑡𝑚 ) ∈ ℐ𝑛+1 , where S𝑘 (𝑥, 𝑦) denotes an S-path of size 𝑘 from 𝑥 to 𝑦. 2. for every 1 ≤ 𝑖 ≤ 𝑚, we have Flood(𝑡𝑖 ) ∈ ℐ𝑛+1 . prop gen Proof sketch. Apart from Rules 𝑅flood and 𝑅flood that relate to the flooding, notice that the first term occurring in an atom of some head also appears as the first term in an atom from the body. The rest follows by induction.
The above guarantees that any element 𝑎𝑖 , as described in Lemma 20, appears exactly at depth 𝑖 in the chase: Lemma 22. Let 𝑎𝑖 be a term from adom(ℐ𝑛 ) as described in Lemma 20, thus with 𝑖 ≤ 𝑛. We have 𝑎𝑖 ∈ adom(ℐ𝑖 ). Proof sketch. We proceed by induction on 𝑖. For 𝑎0 , the claim is trivial as 𝑎0 ∈ adom(ℐ). For 𝑎𝑖+1 , we know it is introduced by applying Rule 𝑅∃ on 𝑎𝑖 (mapping 𝑦 to 𝑎𝑖 ), thus relying on an atom G(𝑎𝑖 , 𝑒) to be satisfied for some End(𝑒) ∈ ℐ. Using Lemma 21, one can establish that G(𝑎𝑖 , 𝑒) ∈ ℐ𝑖 , thus 𝑎𝑖+1 is introduced at step 𝑖 + 1.
ℐ
𝑎
S0
𝑒 S0
S0 S0
𝑓
𝑎1
S0
𝑏1
S0
𝑏2
S0
𝑐1
S0
𝑐2
S0
𝑏
𝑑
S0
S0
S0 S0
𝑐
S0
𝑐3
End Figure 3: Representation of predicates S0 and End in ℐ∞ under the hypothesis that 𝒢 is bounded by 2. The magenta boxed part of the figure is the instance ℐ. The S0 -atoms, as described in Lemma 20, form several chains leading to elements of ℐ. Each of the S0 -chains only grows until the distance to the End-predicate is bigger than the bound on 𝒢 (here 2).
To proceed with the construction of homomorphism ℎ : 𝑞 → ℐ𝑀 as previously sketched. We thus decompose the homomorphism ℎ : 𝑞 → ℐ𝑁 to identify which parts of 𝑞 are mapped along S0 -S-chains. To do so, we define the {S0 , S}-graph of an instance 𝒥 : its nodes are elements of adom(𝒥 ) and there is an edge from 𝑎 to 𝑏 if and only if S0 (𝑎, 𝑏) or S(𝑎, 𝑏) belongs to 𝒥 . We denote this graph by 𝐺𝒥 S,S0 . We then consider weakly connected components (WCC) of this graph. Two terms 𝑎 and 𝑏 are in the same WCC if there is an undirected path from 𝑎 to 𝑏 in 𝐺𝒥 S,S0 . We now come back to defining ℎ′ . Let 𝑉1 , . . . , 𝑉ℓ be the WCCs of 𝐺𝑞S,S0 . We apply Lemma 20 to ℐ𝑁 and obtain the terms as described in its statement. For each 1 ≤ 𝑙 ≤ ℓ, let 𝑑𝑙 be the minimum 𝑑 such that ℎ(𝑣) = 𝑎𝑑 for some 𝑣 ∈ 𝑉𝑙 and 𝑎 ∈ adom(ℐ). We define the mapping ℎ′ : Vars(𝑞) → adom(ℐ𝑀 ) by ‘shifting’ each WCC forward along the chain it lies on, unless it is already close to ℐ: {︂ ℎ(𝑣) if 𝑑𝑙 ≤ |𝑞| where 𝑣 ∈ 𝑉𝑙 ′ ℎ (𝑣) := 𝑎𝑖−𝑑𝑙 otherwise, if ℎ(𝑣) = 𝑎𝑖 and 𝑣 ∈ 𝑉𝑙 ′
We first verify that ℎ′ indeed maps elements within adom(ℐ𝑀 ). Consider a variable 𝑣 of 𝑞 and let 𝑉𝑙 be its WCC in 𝐺𝑞S,S0 . Let 𝑣𝑚𝑖𝑛 be the variable of 𝑉𝑙 that realizes 𝑑𝑙 , for which ℎ(𝑣𝑚𝑖𝑛 ) = 𝑎𝑑𝑙 for some 𝑎 ∈ adom(ℐ). By definition of 𝑉𝑙 , there exists an undirected (simple) path in 𝐺𝑞S,S0 from 𝑣 to 𝑣𝑚𝑖𝑛 , whose length is at most |𝑞|. From ℎ being a homomorphism, the atoms that form this path are mapped via ℎ on atoms described by Lemma 20. It is thus clear that ℎ(𝑣) is some 𝑎𝑖 for 𝑎 ∈ adom(ℐ) and 0 ≤ 𝑖 ≤ 𝑑𝑙 + |𝑞|. Now, if 𝑑𝑙 ≤ |𝑞|, then ℎ′ (𝑣) = ℎ(𝑣) = 𝑎𝑖 and we have 𝑖 ≤ 2 |𝑞|. Otherwise ℎ′ (𝑣) = 𝑎𝑖−𝑑𝑙 and 𝑖 − 𝑑𝑙 ≤ |𝑞| ≤ 2 |𝑞|. In both cases, Lemma 22 warrants ℎ′ (𝑣) ∈ adom(ℐ𝑀 ). We now claim that ℎ′ is a homomorphism from 𝑞 to ℐ𝑀 . Let us denote the restriction of ℐ𝑁 to adom(ℐ𝑛 ) for some 𝑛 ≤ 𝑁 by ℐ𝑁 |𝑛 . We actually prove that ℎ′ is a homomorphism from 𝑞 to ℐ𝑁 |𝑀 −1 . This is sufficient as all atoms from ℐ𝑁 that only involve terms from adom(ℐ𝑀 −1 ) are already in ℐ𝑀 . This is stated in the following lemma, whose proof is by induction and heavily relies on the previous lemmas: Lemma 23. For every 𝑛 ≥ 𝑀 , ℐ𝑛 |𝑀 −1 = ℐ𝑀 |𝑀 −1 . In particular, for 𝑛 = 𝑁 we have ℐ𝑁 |𝑀 −1 = ℐ𝑀 |𝑀 −1 .
We finally prove that ℎ′ is a homomorphism from 𝑞 to ℐ𝑁 |𝑀 −1 . Since End-atoms cannot be introduced during the chase, any End-atom End(𝑡) is mapped through ℎ to an atom of ℐ, and thus ℎ′ (𝑡) = ℎ(𝑡), so End(ℎ′ (𝑡)) ∈ ℐ𝑁 |𝑀 −1 . The case of S0 - and S-atoms is also easy: consider an atom P(𝑡, 𝑡′ ) ∈ 𝑞 for P ∈ {S0 , S}. By definition, 𝑡 and 𝑡′ belong to a same WCC 𝑉𝑙 . If ℎ and ℎ′ coincide on 𝑉𝑙 (that is the case if 𝑑𝑙 ≤ |𝑞|), then P(ℎ′ (𝑡), ℎ′ (𝑡′ )) immediately belongs to ℐ𝑀 via Lemma 23. Otherwise, ℎ(𝑡) = 𝑎𝑖 and ℎ(𝑡′ ) = 𝑎𝑗 for some 𝑎 ∈ adom(ℐ) and 𝑖, 𝑗 such that 𝑖 = 𝑗 + 1 or 𝑖 = 𝑗 − 1 by Lemma 20. Thus, ℎ′ (𝑡) = 𝑎𝑖−𝑑𝑙 and ℎ′ (𝑡′ ) = 𝑎𝑗−𝑑𝑙 , and 𝑖 − 𝑑𝑙 and 𝑗 − 𝑑𝑙 satisfy the same relation and are smaller than 𝑀 , so P(ℎ′ (𝑡), ℎ′ (𝑡′ )) belongs to ℐ𝑀 . It remains to treat the case of atoms based upon other predicates. Consider an atom P(𝑡1 , . . . , 𝑡𝑚 ) ∈ 𝑞 for some P∈ / {S0 , S} of arity 𝑚. Since ℎ is a homomorphism, we have P(ℎ(𝑡1 ), . . . , ℎ(𝑡𝑚 )) ∈ ℐ𝑁 . If all ℎ(𝑡𝑖 ) ∈ adom(ℐ), then all ℎ′ (𝑡𝑖 ) = ℎ(𝑡𝑖 ) and we are done. Otherwise, we can apply Lemma 21. In the case where ℎ(𝑡𝑖 ) are all gen flooded, then so are the ℎ′ (𝑡𝑖 ) and Rule 𝑅flood concludes. Otherwise, all ℎ(𝑡𝑖 ) belong to the same WCC 𝑉𝑙 . Again, if 𝑑𝑙 ≤ |𝑞|, then ℎ′ and ℎ coincide on 𝑉𝑙 and we are done. Otherwise, all 𝑡𝑖 ’s map to some 𝑎𝑘𝑖 for 𝑎 ∈ adom(ℐ) and prop 𝑘𝑖 < 𝑚𝑎 , since 𝑎𝑘𝑖 +𝑑𝑙 ∈ adom(ℐ𝑁 ). Thus, by Rule 𝑅flood , gen ′ ℎ (𝑡𝑖 ) is flooded, and thus again Rule 𝑅flood concludes.
6
Conclusion
We have shown that decidable BCQ entailment does not imply the decidability of bts membership or chase termination for concrete classes of existential rules. This explains the necessity of diverse, class-specific techniques for proving termination, as BCQ entailment offers no systematic tool for this purpose. Future work includes proving that entailment of recursive C2RPQs is also decidable for the class presented here. Conversely, it remains an open problem to identify a homomorphism-closed query language whose decidable entailment is sufficient to guarantee the decidability of chase termination.
Acknowledgments This work has been partially supported by ANR grant EXPAND (ANR-25-CE23-1215). The authors would like
to thank David Carral who hinted this topic and provided useful insights. He still has not played Celeste though.
References [Afrati and Kolaitis, 2008] Foto Afrati and Phokion G. Kolaitis. Answering aggregate queries in data exchange. In Proceedings of the 27th ACM SIGMOD-SIGACTSIGART Symposium on Principles of Database Systems, PODS’08, page 129–138. Association for Computing Machinery, 2008. [Baget et al., 2009] Jean-François Baget, Michel Leclère, Marie-Laure Mugnier, and Êric Salvat. Extending decidable cases for rules with existential variables. In Proceedings of the 21st International Joint Conference on Artificial Intelligence, IJCAI’09, page 677–682. Morgan Kaufmann Publishers Inc., 2009. [Beeri and Vardi, 1981] Catriel Beeri and Moshe Y. Vardi. The implication problem for data dependencies. In Proceedings of the 8th Colloquium on Automata, Languages and Programming, ICALP’81, page 73–85. Springer-Verlag, 1981. [Calautti and Pieris, 2019] Marco Calautti and Andreas Pieris. Oblivious chase termination: The sticky case. In Proceedings of the 22nd International Conference on Database Theory, ICDT’19, pages 17:1–17:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2019. [Calautti et al., 2015] Marco Calautti, Georg Gottlob, and Andreas Pieris. Chase termination for guarded existential rules. In Proceedings of the 34th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS’15, page 91–103. Association for Computing Machinery, 2015. [Calì et al., 2013] Andrea Calì, Georg Gottlob, and Michael Kifer. Taming the infinite chase: Query answering under expressive relational constraints. J. Artif. Intell. Res., 48:115–174, 2013. [Calì et al., 2012] Andrea Calì, Georg Gottlob, and Thomas Lukasiewicz. A general datalog-based framework for tractable query answering over ontologies. Journal of Web Semantics, 14:57–83, 2012. [Carral et al., 2022] David Carral, Lucas Larroque, Marie-Laure Mugnier, and Michaël Thomazo. Normalisations of existential rules: Not so innocuous! In Proceedings of the 19th International Conference on Principles of Knowledge Representation and Reasoning, KR’22, pages 102–111, 2022. [Courcelle, 1990] Bruno Courcelle. The monadic secondorder logic of graphs. I. recognizable sets of finite graphs. Inf. Comput., 85(1):12–75, 1990. [Delivorias et al., 2021] Stathis Delivorias, Michel Leclère, Marie-Laure Mugnier, and Federico Ulliana. Characterizing boundedness in chase variants. Theory Pract. Log. Program., 21(1):51–79, 2021. [Deutsch et al., 2008] Alin Deutsch, Alan Nash, and Jeff Remmel. The chase revisited. In Proceedings of the
27th ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS’08, page 149–158. Association for Computing Machinery, 2008. [Fagin et al., 2005a] Ronald Fagin, Phokion G. Kolaitis, Renée J. Miller, and Lucian Popa. Data exchange: semantics and query answering. Theoretical Computer Science, 336(1):89–124, 2005. Database Theory. [Fagin et al., 2005b] Ronald Fagin, Phokion G. Kolaitis, and Lucian Popa. Data exchange: getting to the core. ACM Trans. Database Syst., 30(1):174–210, 2005. [Fagin, 2018] Ronald Fagin. Tuple-generating dependencies. In Encyclopedia of Database Systems, Second Edition. Springer, 2018. [Feier et al., 2023] Cristina Feier, Carsten Lutz, and Marcin Przybylko. Answer counting under guarded tgds. Log. Methods Comput. Sci., 19(3), 2023. [Gaifman et al., 1993] Haim Gaifman, Harry G. Mairson, Yehoshua Sagiv, and Moshe Y. Vardi. Undecidable optimization problems for database logic programs. J. ACM, 40(3):683–713, 1993. [Gerlach et al., 2025] Lukas Gerlach, Lucas Larroque, Jerzy Marcinkowski, and Piotr Ostropolski-Nalewaja. About the multi-head linear restricted chase termination. In Proceedings of the 22nd International Conference on Principles of Knowledge Representation and Reasoning, KR’25, pages 346–355, 2025. [Gogacz and Marcinkowski, 2014] Tomasz Gogacz and Jerzy Marcinkowski. All-instances termination of chase is undecidable. In Proceedings of the 41st International Colloquium on Automata, Languages, and Programming, ICALP’14, pages 293–304. Springer, 2014. [Gogacz et al., 2020] Tomasz Gogacz, Jerzy Marcinkowski, and Andreas Pieris. All-instances restricted chase termination. In Proceedings of the 39th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS’20, page 245–258. Association for Computing Machinery, 2020. [Hernich, 2012] André Hernich. Computing universal models under guarded tgds. In Proceedings of the 15th International Conference on Database Theory, ICDT’12, page 222–235. Association for Computing Machinery, 2012. [Maier et al., 1979] David Maier, Alberto O. Mendelzon, and Yehoshua Sagiv. Testing implications of data dependencies. ACM Trans. Database Syst., 4(4):455–469, 1979. [Marnette, 2009] Bruno Marnette. Generalized schemamappings: from termination to tractability. In Proceedings of the 28th ACM SIGMOD-SIGACTSIGART Symposium on Principles of Database Systems, PODS’09, page 13–22. Association for Computing Machinery, 2009. [Minsky, 1967] Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, 1967.
[Ronca et al., 2018] Alessandro Ronca, Mark Kaminski, Bernardo Cuenca Grau, Boris Motik, and Ian Horrocks. Stream reasoning in temporal datalog. In Proceedings of the 32nd AAAI Conference on Artificial Intelligence, AAAI’18, pages 1941–1948. AAAI Press, 2018.
A
Proofs for Section 4 (Undecidability of Chase Termination and bts-Recognition)
X Lemma 12. For all 𝑛 > 0, if ChX 𝑛 (ℐE ) ̸= Ch𝑛−1 (ℐE ), X then adom(Ch𝑛 (ℐE )) = {𝑡0 , . . . , 𝑡𝑛−1 , 𝑤} for some terms 𝑡0 , . . . , 𝑡𝑛−1 , and the S0 -atoms of ChX 𝑛 (ℐE ) are exactly { S0 (𝑡𝑖 , 𝑡𝑖+1 ) | 0 ≤ 𝑖 < 𝑛 } where 𝑡𝑛 = 𝑤.
Proof. By induction on 𝑛. For the base case (𝑛 = 1), notice that ChX = 0 (ℐE ) {End(𝑤), S(𝑤, 𝑤), Flood(𝑤), G(𝑤, 𝑤)} ∪ prop { R𝑖 (𝑤, 𝑤), T𝑖 (𝑤, 𝑤, 𝑤) | 𝑖 < 𝑝 } by Rules 𝑅SEnd , 𝑅flood gen X and 𝑅flood . Thus, if ChX 1 (ℐE ) ̸= Ch0 (ℐE ), Rule 𝑅∃ (the only existential rule) must have been applied, and created S0 (𝑡0 , 𝑤) for some fresh term 𝑡0 , so adom(ChX 1 (ℐE )) = {𝑡0 , 𝑤}. Since no Datalog rule can yield S0 -atoms, the only S0 -atom is S0 (𝑡0 , 𝑤), as required. For the inductive step, assume that the result holds X for some 𝑛 ≥ 1 and that ChX 𝑛+1 (ℐE ) ̸= Ch𝑛 (ℐE ). By the induction hypothesis, there are terms 𝑡′0 , . . . , 𝑡′𝑛−1 ′ ′ such that adom(ChX 𝑛 (ℐE )) = {𝑡0 , . . . , 𝑡𝑛−1 , 𝑤} and the S0 X ′ ′ atoms of Ch𝑛 (ℐE ) are exactly { S0 (𝑡𝑖 , 𝑡𝑖+1 ) | 0 ≤ 𝑖 < 𝑛 }. As there is a single existential rule in ℛℳ , all terms 𝑡′𝑖 have been generated by Rule 𝑅∃ where 𝑦 is mapped to 𝑡′𝑖+1 (and to 𝑤 for 𝑡′𝑛−1 ). Thus, the only way for X ChX 𝑛+1 (ℐE ) to differ from Ch𝑛 (ℐE ) is for Rule 𝑅∃ to be ′ applied by mapping 𝑦 to 𝑡0 , creating a new term 𝑡0 and the atom S0 (𝑡0 , 𝑡′0 ). Let 𝑡𝑖 = 𝑡′𝑖−1 for all 1 ≤ 𝑖 ≤ 𝑛, so that adom(ChX 𝑛 (ℐE )) = {𝑡1 , . . . , 𝑡𝑛 , 𝑤}. Since no Datalog rule can yield S0 -atoms, the only S0 -atoms of ChX 𝑛+1 (ℐE ) are exactly { S0 (𝑡𝑖 , 𝑡𝑖+1 ) | 0 ≤ 𝑖 < 𝑛 + 1 }, as required. X Lemma 13. For all 𝑛 > 0, if ChX 𝑛 (ℐE ) ̸= Ch𝑛−1 (ℐE ),
(i) R𝑖 (𝑡0 , 𝑡𝑘 ) ∈ ChX 𝑛 (ℐE ) if and only if 𝑘 = 𝑖 mod 𝑝; (ii) T𝑖 (𝑡0 , 𝑡𝑘 , 𝑡𝑙 ) ∈ ChX 𝑛 (ℐE ) if and only if there is 𝑚 such that 𝑘 = 𝑚𝑟𝑖 and 𝑙 = 𝑚𝑞𝑖 ; (iii) For all 𝑘 ∈ N, G(𝑡0 , 𝑡𝑔𝑘 (2) ) ∈ ChX 𝑛 (ℐE ); (iv) If 𝒢 is bounded by 𝑛 − 1, then for all 𝑙 such that 𝑘 G(𝑡0 , 𝑡𝑙 ) ∈ ChX 𝑛 (ℐE ), there is 𝑘 such that 𝑙 = 𝑔 (2). Proof. For Item (i), we proceed by induction on 𝑘. Initially, when 𝑡0 is created by Rule 𝑅∃ , there is only R0 (𝑡0 , 𝑡0 ). Then, Flood(𝑡0 ) ∈ / ChX 𝑛 (ℐE ) by Lemma 12 and prop the fact that only Rule 𝑅flood can create Flood-atoms. Thus, only Rule 𝑅R,𝑖 can generate new R𝑖 -atoms with 𝑡0 as first argument. By induction, assume that 𝑘 − 1 = 𝑖 mod 𝑝, and thus that R𝑖 (𝑡0 , 𝑡𝑘−1 ) ∈ ChX 𝑛 (ℐE ), for some 𝑘 ∈ N. Then, since S(𝑡𝑘−1 , 𝑡𝑘 ) ∈ ChX (ℐ ), Rule 𝑅R,𝑖 creE 𝑛 ates R(𝑖+1) mod 𝑝 (𝑡0 , 𝑡𝑘+1 ), as required. Since no other rule can create R𝑖 -atoms with 𝑡0 as first argument, Item (i) holds. For Item (ii), we proceed by induction on 𝑚. Initially, when 𝑡0 is created by Rule 𝑅∃ , there is only T𝑖 (𝑡0 , 𝑡0 , 𝑡0 )
for all 𝑖 < 𝑝. Then, as before, Flood(𝑡0 ) ∈ / ChX 𝑛 (ℐE ), so only Rule 𝑅T,𝑖 can generate new T𝑖 -atoms with 𝑡0 as first argument. By induction, assume that 𝑘 = 𝑚𝑟𝑖 and 𝑙 = 𝑚𝑞𝑖 , for some 𝑖 < 𝑝 and 𝑘, 𝑙. Then, since S𝑟𝑖 (𝑡𝑘 , 𝑡𝑘+𝑟𝑖 ) and S𝑞𝑖 (𝑡𝑙 , 𝑡𝑙+𝑞𝑖 ) belong to ChX 𝑛 (ℐE ), Rule 𝑅T,𝑖 creates T𝑖 (𝑡0 , 𝑡𝑘+𝑟𝑖 , 𝑡𝑙+𝑞𝑖 ). As 𝑘 + 𝑟𝑖 = (𝑚 + 1)𝑟𝑖 and 𝑙 + 𝑞𝑖 = (𝑚 + 1)𝑞𝑖 , and no other rule can create T𝑖 -atoms with 𝑡0 as first argument, Item (ii) holds. For Item (iii), we proceed by induction on 𝑘. For the base case (𝑘 = 0), Rule 𝑅Ginit creates G(𝑡0 , 𝑡𝑔0 (2) ) = G(𝑡0 , 𝑡2 ). For the inductive step, assume that the result holds for some 𝑘 ∈ N and let 𝑙 = 𝑔 𝑘 (2). By the induction ′ 𝑘+1 hypothesis, G(𝑡0 , 𝑡𝑙 ) ∈ ChX (2) = 𝑛 (ℐE ). Then, let 𝑙 = 𝑔 𝑞𝑖 𝑔(𝑙) = 𝑙 𝑟𝑖 for 𝑖 = 𝑙 mod 𝑝. By Item (i) above, R𝑖 (𝑡0 , 𝑡𝑙 ) ∈ 𝑟𝑖 𝑙 ChX 𝑛 (ℐE ). Then, since 𝑙′ = 𝑞𝑖 , there is some 𝑚 such that 𝑙 = 𝑚𝑟𝑖 and 𝑙′ = 𝑚𝑞𝑖 . Thus, by Item (ii) above, step T𝑖 (𝑡0 , 𝑡𝑙 , 𝑡𝑙′ ) ∈ ChX 𝑛 (ℐE ). Thus, by Rule 𝑅G,𝑖 , G(𝑡0 , 𝑡𝑙′ ) = G(𝑡0 , 𝑡𝑔𝑘+1 (2) ) ∈ ChX 𝑛 (ℐE ), as required. For Item (iv), we prove that if 𝒢 is bounded by 𝑛 − 1, step then the only G-atom that can be generated by Rule 𝑅G,𝑖 by mapping 𝑦 to 𝑡𝑔𝑘 (2) is G(𝑡0 , 𝑡𝑔𝑘+1 (2) ). Since 𝒢 is bounded by 𝑛 − 1, by Item (i), the only 𝑖 such that 𝑘 R𝑖 (𝑡0 , 𝑡𝑔𝑘 (2) ) ∈ ChX 𝑛 (ℐE ) is 𝑖 = 𝑔 (2) mod 𝑝. Then, by Item (ii), the only T𝑖 -atom that features 𝑡𝑔𝑘 (2) in second position is T𝑖 (𝑡0 , 𝑡𝑔𝑘 (2) , 𝑡𝑔𝑘+1 (2) ). Thus, the only G-atom step that can be generated by Rule 𝑅G,𝑖 by mapping 𝑦 to 𝑡𝑔𝑘 (2) is G(𝑡0 , 𝑡𝑔𝑘+1 (2) ), as required. Thus, by induction on 𝑘, the only G-atoms with 𝑡0 as first argument are those of the form G(𝑡0 , 𝑡𝑔𝑘 (2) ), as required. Theorem 14. If ℳ does not halt, there is no terminating X-chase sequence from ⟨{End(𝑤)}, ℛℳ ⟩. Proof of Theorem 14. We prove by induction on 𝑛 that if 𝒢 is unbounded (which coincides with ℳ not halting by Proposition 11), then Rule 𝑅∃ is E-applicable (and thus X-applicable for all variants X) on ChX 𝑛 (ℐE ). For the base case, note that ChX = 0 (ℐE ) {End(𝑤), S(𝑤, 𝑤), Flood(𝑤), G(𝑤, 𝑤)} ∪ { R𝑖 (𝑤, 𝑤), T𝑖 (𝑤, 𝑤, 𝑤) | 𝑖 < 𝑝 }, as highlighted in the proof of Lemma 12. Thus, Rule 𝑅∃ is applicable on X ChX 0 (ℐE ). Since there is no S0 -atom in Ch0 (ℐE ), there is no way to homomorphically map the fresh term created by Rule 𝑅∃ to any existing term, so the rule is indeed E-applicable. For the inductive step, assume that the result holds X for some 𝑛 ≥ 0. Thus, ChX 𝑛+1 (ℐE ) ̸= Ch𝑛 (ℐE ) by the induction hypothesis, so by Lemma 12, there are terms 𝑡0 , . . . , 𝑡𝑛 such that adom(ChX 𝑛+1 (ℐE )) = {𝑡0 , . . . , 𝑡𝑛 , 𝑤} X and the S0 -atoms of Ch𝑛+1 (ℐE ) are exactly { S(𝑡𝑖 , 𝑡𝑖+1 ) | 0 ≤ 𝑖 < 𝑛 + 1 }. Thus, by Rule 𝑅S , for all 𝑘 > 𝑛 + 1, S𝑘 (𝑡0 , 𝑤) ∈ ChX 𝑛+1 (ℐE ). Since 𝒢 is unbounded, there is some 𝑘 such that 𝑔 𝑘 (2) > 𝑛 + 1. Hence, by Item (iii) of Lemma 13, G(𝑡0 , 𝑤) ∈ ChX 𝑛+1 (ℐE ). Then, since End(𝑤) ∈
X ChX 𝑛+1 (ℐE ), Rule 𝑅∃ is applicable on Ch𝑛+1 (ℐE ) by mapping 𝑦 to 𝑡𝑔𝑘 (2) . Since by construction, the S0 -atoms of ChX 𝑛+1 (ℐE ) are exactly { S0 (𝑡𝑖 , 𝑡𝑖+1 ) | 0 ≤ 𝑖 < 𝑛 }, there is no way to homomorphically map the result of applying 𝑅∃ into ChX 𝑛+1 (ℐE ), so the rule is indeed E-applicable. Thus, this proves that at each step, Rule 𝑅∃ is E-applicable, so the E-chase does not terminate on ⟨{End(𝑤)}, ℛℳ ⟩. This entails that no X-chase sequence from ⟨{End(𝑤)}, ℛℳ ⟩ terminates, as the E-chase terminates if and only if a universal model exists [Deutsch et al., 2008], and any other variant terminating would yield such a model.
Lemma 15. For all 𝑛 ∈ N, 𝒥𝑛 ≃ ChO 𝑛 (ℐE ) ∪ {S0 (𝑤, 𝑤)}. Proof. By induction on 𝑛. For the base case (𝑛 = 0), note that ChO 0 (ℐE ) = {End(𝑤), S(𝑤, 𝑤), Flood(𝑤), G(𝑤, 𝑤)} ∪ prop { R𝑖 (𝑤, 𝑤), T𝑖 (𝑤, 𝑤, 𝑤) | 𝑖 < 𝑝 } by Rules 𝑅SEnd , 𝑅flood and gen 𝑅flood . Since the critical instance contains all possible facts over the schema, 𝒥0 = 𝒥 = ChO 0 (ℐE ) ∪ {S0 (𝑤, 𝑤)}, as required. For the inductive step, assume that the result holds for some 𝑛 ≥ 0. Thus, 𝒥𝑛 ≃ ChO 𝑛 (ℐE ) ∪ {S0 (𝑤, 𝑤)}. The only possible trigger that can use S0 (𝑤, 𝑤) uses Rule 𝑅S to produce S(𝑤, 𝑤), which is already present in 𝒥. Thus, all other triggers are either applicable on both instances or on none of them, and produce the same atoms, so 𝒥𝑛+1 ≃ ChO 𝑛+1 (ℐE ) ∪ {S0 (𝑤, 𝑤)}, as required. Theorem 16. If ℳ halts, then the X-chase terminates on ⟨ℐ, ℛℳ ⟩ for all instances ℐ. Proof of Theorem 16. We use the notations of Lemma 12 to designate the terms of 𝒥𝑛 , since according to Lemma 15, it is isomorphic to ChO 𝑛 (ℐE ) ∪ {S0 (𝑤, 𝑤)}. Assume that 𝒢 is bounded by 𝑛 ∈ N. By Items (iii) and (iv) of Lemma 13, all G-atoms of 𝒥𝑛+1 with 𝑡0 as first argument are of the form G(𝑡0 , 𝑡𝑔𝑘 (2) ) for some 𝑘, such that 𝑔 𝑘 (2) ≤ 𝑛. Thus, in particular, G(𝑡0 , 𝑤) ∈ / 𝒥𝑛+1 , so Rule 𝑅∃ is not applicable on 𝒥𝑛+1 . Since it is the only existential rule in ℛℳ , the O-chase terminates on ⟨𝒥0 , ℛℳ ⟩ by step 𝑛 + 1. Thus, by the initial remarks of this section, the X-chase terminates on ⟨ℐ, ℛℳ ⟩ for all instances ℐ.
B
Proofs for Section 5 (Decidability of BCQ Entailment)
Lemma 20. For all 𝑛 ≥ 0 and 𝑎 ∈ adom(ℐ), there exist integers 0 ≤ 𝑚𝑎 ≤ 𝑛 s.t.: (i) the domain of ℐ𝑛 consists of distinct terms 𝑎𝑖 with 𝑎 ∈ adom(ℐ) and 0 ≤ 𝑖 ≤ 𝑚𝑎 , and where 𝑎0 = 𝑎; and (ii) S0 atoms of ℐ𝑛 are exactly: {S0 (𝑎, 𝑏) | S0 (𝑎, 𝑏) ∈ ℐ} ∪ {S0 (𝑎𝑖+1 , 𝑎𝑖 ) | 0 ≤ 𝑖 < 𝑚𝑎 , 𝑎 ∈ adom(ℐ)}, and, as a corollary, the S atoms of ℐ𝑛 are exactly: {S(𝑎, 𝑏) | S(𝑎, 𝑏) ∈ ℐ or S0 (𝑎, 𝑏) ∈ ℐ} ∪ {S(𝑎, 𝑎) | End(𝑎) ∈ ℐ} ∪ {S(𝑎𝑖+1 , 𝑎𝑖 ) | 0 ≤ 𝑖 < 𝑚𝑎 , 𝑎 ∈ adom(ℐ)}.
Proof. We proceed by induction on 𝑛 ≥ 0. For 𝑛 = 0, it suffices to set 𝑚𝑎 = 0 for every 𝑎 ∈ adom(ℐ). Since we only applied our Datalog rules on SO ∀ ℐ (recall that ℐ0 = ChX 0 (ℐ) = Ch (ℐ, ℛℳ ) by definition), it is clear that Point (𝑖) is satisfied: adom(ℐ0 ) = adom(ℐ). For Point (𝑖𝑖), notice that no rule from ℛ∀ℳ allows introducing an S0 atom, hence the S0 -atoms of ℐ0 are exactly {S0 (𝑎, 𝑏) | S0 (𝑎, 𝑏) ∈ ℐ}, as claimed. Regarding the S atoms, notice that the claimed expression exactly accounts for applications of Rules 𝑅S and 𝑅SEnd . Let us now assume that the claim holds at some step 𝑛 ≥ 0 and let us consider ℐ𝑛+1 . We apply the induction hypothesis on ℐ𝑛 and denote 𝑚𝑛,𝑎 the obtained integers, for 𝑎 ∈ adom(ℐ). As there is a single existential rule in ℛℳ , every term 𝑎𝑖 of adom(ℐ𝑛 ), for 𝑎 ∈ adom(ℐ) and 0 < 𝑖 ≤ 𝑚𝑛,𝑎 has been generated by rule 𝑅∃ with 𝑦 necessarily mapped to 𝑎𝑖−1 due to the description of S0 we have in ℐ𝑛 . Therefore, a trigger for 𝑅∃ mapping 𝑦 on such a term 𝑎𝑖 is no longer SO-applicable unless 𝑖 = 𝑚𝑛,𝑎 . In that case, each such application of 𝑅∃ produces a new term 𝑎𝑚𝑛,𝑎 +1 , along with the atom S0 (𝑎𝑚𝑛,𝑎 +1 , 𝑎𝑚𝑛,𝑎 ). Note that there cannot be any further trigger for 𝑅∃ on the freshly introduced term 𝑎𝑚𝑛,𝑎 +1 as 𝑅∃ does not introduce the necessary G atom. Therefore, we can set 𝑚𝑎 := 𝑚𝑛,𝑎 + 1 whenever such a fresh element is introduced. Notice that the induction hypothesis guarantees 𝑚𝑛,𝑎 ≤ 𝑛, so that 𝑚𝑎 ≤ 𝑛 + 1 as desired for Point (𝑖). For Point (𝑖𝑖), note that such applications of 𝑅∃ are the only way to produce more S0 atoms, so that the description of S0 atoms (and subsequently of S atoms), is correct. We now state a direct corollary of Lemma 20 which provides a similar full-characterization for the predicate Flood. This lemma allows to simplify the presentation of the proof of Lemma 21 further in this appendix. Corollary 24. Let 𝑛 ≥ 0 and consider the terms of adom(ℐ𝑛 ) as described in Lemma 20. The Flood atoms of ℐ𝑛 are exactly: {Flood(𝑎) | Flood(𝑎) ∈ ℐ or End(𝑎) ∈ ℐ} ∪ {Flood(𝑎) | S(𝑏, 𝑎) ∈ ℐ or S0 (𝑏, 𝑎) ∈ ℐ} ∪ {Flood(𝑎𝑖 ) | 0 ≤ 𝑖 < 𝑚𝑎 , 𝑎 ∈ adom(ℐ)}. Proof. This is a direct consequence of the description of the S-atoms given by Lemma 20 joint with the observation that a Flood-atom can only be produced by an prop application of Rule 𝑅flood . Lemma 21. Let 𝑛 ≥ 0 and P(𝑡1 , . . . , 𝑡𝑚 ) an atom. If P(𝑡1 , . . . , 𝑡𝑚 ) ∈ ℐ𝑛+1 ∖ ℐ𝑛 then one of the following holds: 1. 𝑡1 ∈ adom(ℐ𝑛+1 ) ∖ adom(ℐ𝑛 ) and there are 𝑘2 ,. . . , 𝑘𝑚 ≥ 0 s.t. S𝑘2 (𝑡1 , 𝑡2 ), . . . , S𝑘𝑚 (𝑡1 , 𝑡𝑚 ) ∈ ℐ𝑛+1 , where S𝑘 (𝑥, 𝑦) denotes an S-path of size 𝑘 from 𝑥 to 𝑦. 2. for every 1 ≤ 𝑖 ≤ 𝑚, we have Flood(𝑡𝑖 ) ∈ ℐ𝑛+1 . Proof. Let 𝑛 ≥ 0. We prove that the derivation leading from ℐ𝑛 to ℐ𝑛+1 only produces atoms that respect the claimed condition. We proceed by induction on this derivation. If the derivation is empty, that is ℐ𝑛+1 = ℐ𝑛 ,
then we are done as ℐ𝑛+1 ∖ ℐ𝑛 = ∅. Otherwise, let us assume that the claimed condition holds for all atoms introduced so far, and let 𝑅 be the next rule to be applied. Assume 𝑅 introduces an atom P(𝑡1 , . . . , 𝑡𝑚 ) ∈ ℐ𝑛+1 ∖ ℐ𝑛 . We treat all nine possible cases for 𝑅. 𝑅S . We have P(𝑡1 , . . . , 𝑡𝑚 ) = S(𝑡1 , 𝑡2 ) and S0 (𝑡1 , 𝑡2 ) has already been derived. If S(𝑡1 , 𝑡2 ) ∈ ℐ𝑛+1 ∖ ℐ𝑛 , we can apply the induction hypothesis which immediately concludes. Otherwise S(𝑡1 , 𝑡2 ) ∈ ℐ𝑛 , but ℐ𝑛 is closed under Datalog rules, thus under Rule 𝑅S and thus S0 (𝑡1 , 𝑡2 ) ∈ ℐ𝑛 , contradiction. 𝑅R,𝑖 . We have P(𝑡1 , . . . , 𝑡𝑚 ) = R𝑖+1 (𝑡1 , 𝑡2 ) and there exists some 𝑡 such that R𝑖 (𝑡1 , 𝑡) and S(𝑡, 𝑡2 ) have already been derived. Notice that, due to S(𝑡, 𝑡2 ) and ℐ𝑛+1 being close under Datalog rules, we have prop Flood(𝑡2 ) ∈ ℐ𝑛+1 due to Rule 𝑅flood . If R𝑖 (𝑡1 , 𝑡) ∈ / ℐ𝑛 , then we can apply the induction hypothesis. In case 𝑡1 ∈ / adom(ℐ𝑛 ), we have S𝑘 (𝑡1 , 𝑡) ∈ ℐ𝑛+1 , thus using S(𝑡, 𝑡2 ) we obtain S𝑘+1 (𝑡1 , 𝑡2 ) ∈ ℐ𝑛+1 as desired. In case Flood(𝑡1 ) ∈ Flood(ℐ𝑛+1 ), recall that also Flood(𝑡2 ) ∈ ℐ𝑛+1 thus we are done. If R𝑖 (𝑡1 , 𝑡) ∈ ℐ𝑛 , note that S(𝑡, 𝑡2 ) ∈ ℐ𝑛 as well using Lemma 20. Therefore Rule 𝑅R,𝑖 was already applicable on ℐ𝑛 which is closed under Datalog rules, so R𝑖+1 (𝑡1 , 𝑡2 ) ∈ ℐ𝑛 , contradiction. 𝑅T,𝑖 . The argument is essentially the same as for 𝑅 = 𝑅R,𝑖 . We have P(𝑡1 , . . . , 𝑡𝑚 ) = T𝑖 (𝑡1 , 𝑡2 , 𝑡3 ) and there exists some terms 𝑠, 𝑠′ such that T𝑖 (𝑡1 , 𝑠, 𝑠′ ), S𝑞𝑖 (𝑠, 𝑡2 ) and S𝑟𝑖 (𝑠′ , 𝑡3 ) have already been derived. Notice again that Flood(𝑡2 ), Flood(𝑡3 ) ∈ ℐ𝑛+1 . If we can apply the induction hypothesis on atom T𝑖 (𝑡1 , 𝑠, 𝑠′ ), we can thus conclude again by composing the S-paths or via Flood(𝑡1 ) ∈ ℐ𝑛+1 . Otherwise we have T𝑖 (𝑡1 , 𝑠, 𝑠′ ) ∈ ℐ𝑛 and thus, using Lemma 20 twice we get S𝑞𝑖 (𝑠, 𝑡2 ), S𝑟𝑖 (𝑠′ , 𝑡3 ) ∈ ℐ𝑛 . We could thus derive T𝑖 (𝑡1 , 𝑡2 , 𝑡3 ) in ℐ𝑛 , contradiction. prop 𝑅flood . We have P(𝑡1 , . . . , 𝑡𝑚 ) = Flood(𝑡1 ) thus Flood(𝑡1 ) ∈ ℐ𝑛+1 and we are done. 𝑅SEnd . We have P(𝑡1 , . . . , 𝑡𝑚 ) = S(𝑡1 , 𝑡1 ) and End(𝑡1 ) has already been derived. Since we cannot produce End using rules, we have End(𝑡1 ) ∈ ℐ, thus S(𝑡1 , 𝑡1 ) ∈ ℐ0 contradicting S(𝑡1 , 𝑡1 ) ∈ / ℐ𝑛 . 𝑅Ginit . We have P(𝑡1 , . . . , 𝑡𝑚 ) = G(𝑡1 , 𝑡2 ) and there exists some 𝑡 such that S(𝑡1 , 𝑡) and S(𝑡, 𝑡2 ) have already been derived. If S(𝑡1 , 𝑡) ∈ / ℐ𝑛 then 𝑡1 ∈ / adom(ℐ𝑛 ) using Lemma 20 and clearly S2 (𝑡1 , 𝑡2 ) ∈ ℐ𝑛+1 as desired. Otherwise S(𝑡1 , 𝑡) ∈ ℐ𝑛 and therefore, using Lemma 20 we have S(𝑡, 𝑡2 ) ∈ ℐ𝑛 as well. Thus Rule 𝑅Ginit is already applicable in ℐ𝑛 , which is closed under Datalog rules thus G(𝑡1 , 𝑡2 ) ∈ ℐ𝑛 , contradiction. step 𝑅G,𝑖 . We have P(𝑡1 , . . . , 𝑡𝑚 ) = G(𝑡1 , 𝑡2 ) and there exists some term 𝑡 such that G(𝑡1 , 𝑡), R𝑖 (𝑡1 , 𝑡) and T𝑖 (𝑡1 , 𝑡, 𝑡2 ) have already been derived. If T𝑖 (𝑡1 , 𝑡, 𝑡2 ) ∈ / ℐ𝑛 , then we can apply the induction hypothesis to it which immediately yields
the desired conclusion. Otherwise we have T𝑖 (𝑡1 , 𝑡, 𝑡2 ) ∈ ℐ𝑛 . If both G(𝑡1 , 𝑡), R𝑖 (𝑡1 , 𝑡) ∈ ℐ𝑛 step then Rule 𝑅G,𝑖 was already applicable in ℐ𝑛 , contradiction. Otherwise we can apply the induction hypothesis to one of these, which gives, in both cases Flood(𝑡1 ), Flood(𝑡) ∈ ℐ𝑛+1 since the case of 𝑡1 ∈ / adom(ℐ𝑛+1 ) would be contradicting T𝑖 (𝑡1 , 𝑡, 𝑡2 ) ∈ ℐ𝑛 . We now consider the introduction of T𝑖 (𝑡1 , 𝑡, 𝑡2 ) ∈ ℐ𝑛 . – If it has been introduced by the application of Rule 𝑅T,𝑖 , then notice that 𝑡3 has a necessary S-predecessor thus Flood(𝑡3 ) ∈ ℐ𝑛+1 and we are done. – If it has been introduced by the application of gen Rule 𝑅flood , then notice that the body guarantees Flood(𝑡3 ) ∈ ℐ𝑛+1 and we are done. – If it has been introduced by the application of Rule 𝑅∃ , then notice that 𝑡1 = 𝑡 = 𝑡3 and since Flood(𝑡1 ) ∈ ℐ𝑛+1 we are done. – Otherwise T𝑖 (𝑡1 , 𝑡, 𝑡2 ) ∈ ℐ, in which case Corollary 24 yields Flood(𝑡1 ), Flood(𝑡) ∈ ℐ0 since Flood(𝑡1 ), Flood(𝑡) ∈ ℐ𝑛+1 Theregen fore, via Rule 𝑅flood and recalling that ℐ0 is closed under Datalog rules, we have G(𝑡1 , 𝑡), R𝑖 (𝑡1 , 𝑡) ∈ ℐ0 ⊆ ℐ𝑛 . We reached a contradiction. gen gen guarantees that Flood(𝑡𝑖 ) has 𝑅flood . The body of 𝑅flood already been derived for all 𝑡𝑖 ’s and thus that Flood(𝑡𝑖 ) ∈ ℐ𝑛+1 for all 𝑡𝑖 ’s as desired.
𝑅∃ . We have P(𝑡1 , . . . , 𝑡𝑚 ) ∈ {S0 (𝑡1 , 𝑡2 ), R0 (𝑡1 , 𝑡1 )} ∪ {T𝑗 (𝑡1 , 𝑡1 , 𝑡1 ) | 1 ≤ 𝑗 ≤ 𝑝 − 1} and 𝑡1 is freshly introduced, thus 𝑡1 ∈ / adom(ℐ𝑛 ). In cases R0 (𝑡1 , 𝑡1 ) and T𝑗 (𝑡1 , 𝑡1 , 𝑡1 ), the claim is trivially true as S0 (𝑡1 , 𝑡2 ) ∈ ℐ𝑛+1 (that is 𝑡1 = 𝑡2 ). For the case P(𝑡1 , . . . , 𝑡𝑚 ) = S0 (𝑡1 , 𝑡2 ), note that it makes the rule 𝑅S applicable. Since we later saturate by Datalog rules in the derivation from ℐ𝑛 to ℐ𝑛+1 , this guarantees that S(𝑡1 , 𝑡2 ) will further be derived due to Rule 𝑅S . Hence S(𝑡1 , 𝑡2 ) ∈ ℐ𝑛+1 as desired.
Lemma 22. Let 𝑎𝑖 be a term from adom(ℐ𝑛 ) as described in Lemma 20, thus with 𝑖 ≤ 𝑛. We have 𝑎𝑖 ∈ adom(ℐ𝑖 ). Proof. We proceed by induction on 𝑛. For 𝑛 = 0, adom(ℐ0 ) = adom(ℐ), so since by definition 𝑎0 = 𝑎 for all 𝑎 ∈ adom(ℐ), the claim holds. Let us assume the claim holds at some step 𝑛 ≥ 0 and consider a term 𝑎𝑖 ∈ adom(ℐ𝑛+1 ). If 𝑎𝑖 ∈ adom(ℐ𝑛 ) then we are done by induction hypothesis. Otherwise 𝑎𝑖 ∈ adom(ℐ𝑛+1 ) ∖ adom(ℐ𝑛 ), thus 𝑎𝑖 has been freshly introduced by some application of 𝑅∃ mapping 𝑦 on some term 𝑡 of ℐ𝑛 and 𝑧 on a term 𝑒 such that G(𝑡, 𝑒), End(𝑒) ∈ ℐ𝑛 (recall that, in the derivation from ℐ𝑛 to ℐ𝑛+1 , we apply first the existential rule 𝑅∃ , which does not produce any G- nor End-atoms, which is why we know G(𝑡, 𝑒), End(𝑒) ∈ ℐ𝑛 ). Using Lemma 20, we deduce
that 𝑖 ≥ 1 and that 𝑡 = 𝑎𝑖−1 . Since 𝑎𝑖−1 ∈ adom(ℐ𝑛 ), by induction hypothesis we obtain 𝑎𝑖−1 ∈ adom(ℐ𝑖−1 ). We now want to prove that G(𝑎𝑖−1 , 𝑒), End(𝑒) ∈ ℐ𝑖−1 . This would conclude as it proves that 𝑅∃ is applicable on ℐ𝑖−1 and therefore that 𝑎𝑖 ∈ adom(ℐ𝑖 ) as desired. Since no rule can ever produce End-atoms, we have End(𝑒) ∈ ℐ, and in particular End(𝑒) ∈ ℐ𝑖−1 . It remains to prove that G(𝑎𝑖−1 , 𝑒) ∈ ℐ𝑖−1 . Let us now set 𝑗 the smallest integer such that G(𝑎𝑖−1 , 𝑒) ∈ ℐ𝑗 (recall we know G(𝑎𝑖−1 , 𝑒) ∈ ℐ𝑛 , so this is well-defined). If 𝑗 = 0, then G(𝑎𝑖−1 , 𝑒) ∈ ℐ0 , thus G(𝑎𝑖−1 , 𝑒) ∈ ℐ𝑖−1 and we are done. Otherwise 𝑗 ≥ 1 and we apply Lemma 21 to the fact G(𝑎𝑖−1 , 𝑒) ∈ ℐ𝑗 ∖ ℐ𝑗−1 . If we are in the case 𝑎𝑖−1 ∈ adom(ℐ𝑗 ) ∖ adom(ℐ𝑗−1 ), then it must be that 𝑗 = 𝑖 − 1 since 𝑎𝑖−1 ∈ adom(ℐ𝑖−1 ), thus G(𝑎𝑖−1 , 𝑒) ∈ ℐ𝑖−1 and we are done. Otherwise we have that Flood(𝑎𝑖−1 ) ∈ ℐ𝑗 . Due to our rules, this is only possible if Flood(𝑎𝑖−1 ) ∈ ℐ or if 𝑎𝑖−1 has an S-predecessor in ℐ𝑗 . In the first case, we have Flood(𝑎𝑖−1 ) ∈ ℐ and recall that End(𝑒) ∈ ℐ. Thus prop gen 𝑅SEnd and 𝑅flood apply on 𝑒 already in ℐ, making 𝑅flood applicable with 𝑥 = 𝑎𝑖−1 , and 𝑦 = 𝑧 = 𝑒, thus producing atom G(𝑎𝑖−1 , 𝑒) already in ℐ0 , and we are done. In the latter case, 𝑎𝑖−1 has an S-predecessor in ℐ𝑗 , which cannot be 𝑎𝑖 yet, so, according to Lemma 20, we have 𝑎𝑖−1 has an S-predecessor in ℐ0 . Here again, 𝑅SEnd applies on 𝑒 prop in ℐ and 𝑅flood apply on both 𝑎𝑖−1 and 𝑒 already in ℐ0 , gen making 𝑅flood applicable with 𝑥 = 𝑎𝑖−1 , and 𝑦 = 𝑧 = 𝑒, thus producing atom G(𝑎𝑖−1 , 𝑒) already in ℐ0 , and we are done. We now state a direct corollary of Lemmas 20 and 22, simply stating that if 𝑡 is the S-predecessor of 𝑡′ , and that 𝑡′ is a term of ℐ𝑛 , then 𝑡 is a term of ℐ𝑛+1 . In the upcoming proof of Lemma 23, it will spare us several case distinctions between terms from ℐ and fresh terms introduced along a chain. Corollary 25. For every 𝑛 ≥ 0, if S(𝑡, 𝑡′ ) ∈ ℐ𝑛 and 𝑡′ ∈ adom(ℐ𝑖 ) for some 0 ≤ 𝑖 ≤ 𝑛, then 𝑡 ∈ adom(ℐ𝑖+1 ). Proof. We first rely on the description of the S-atoms in ℐ𝑛 . If both 𝑡, 𝑡′ ∈ adom(ℐ), the claim is clear. Otherwise 𝑡 = 𝑎𝑗+1 and 𝑡′ = 𝑎𝑗 for some 0 ≤ 𝑗 ≤ 𝑛 and 𝑎 ∈ adom(ℐ). We have 𝑎𝑗 ∈ adom(ℐ𝑖 ) by assumption, thus 𝑗 ≤ 𝑖 by Lemma 20 applied to ℐ𝑖 . Therefore 𝑗 + 1 ≤ 𝑖 + 1 and Lemma 22 now gives 𝑡 = 𝑎𝑗+1 ∈ adom(ℐ𝑖+1 ) as desired. Lemma 23. For every 𝑛 ≥ 𝑀 , ℐ𝑛 |𝑀 −1 = ℐ𝑀 |𝑀 −1 . In particular, for 𝑛 = 𝑁 we have ℐ𝑁 |𝑀 −1 = ℐ𝑀 |𝑀 −1 . Proof. Notice that ℐ𝑀 −1 is well-defined since 𝑀 ≥ 1. We proceed by induction on 𝑛. For 𝑛 = 𝑀 , the claim is trivial. Let us now assume that the claim holds until some 𝑛 ≥ 𝑀 , that is we have ℐ𝑛 |𝑀 −1 = ℐ𝑀 |𝑀 −1 . Notice that ℐ𝑛+1 |𝑀 −1 ⊇ ℐ𝑀 |𝑀 −1 is by definition; it remains to prove ℐ𝑛+1 |𝑀 −1 ⊆ ℐ𝑀 |𝑀 −1 . We proceed by induction on the derivation 𝐷 that leads from ℐ𝑛 |𝑀 −1 to ℐ𝑛+1 |𝑀 −1 . If 𝐷 is empty, we have ℐ𝑛+1 |𝑀 −1 = ℐ𝑛 |𝑀 −1 and the claim holds by the induction hypothesis on 𝑛. Otherwise, let
us assume that the claim holds for all atoms of ℐ𝑛+1 |𝑀 −1 introduced so far by 𝐷, and let 𝑅 be the next rule to be applied. Assume the application of 𝑅 leads to the introduction of an atom P(𝑡0 , . . . , 𝑡𝑚 ) ∈ ℐ𝑛+1 with 𝑡𝑖 ∈ adom(ℐ𝑀 −1 ) for every 1 ≤ 𝑖 ≤ 𝑚. We treat all nine possible cases for 𝑅. 𝑅S . We have P(𝑡1 , . . . , 𝑡𝑚 ) = S(𝑡1 , 𝑡2 ) and S0 (𝑡1 , 𝑡2 ) has already been derived. In particular, S0 (𝑡1 , 𝑡2 ) ∈ ℐ𝑛+1 . Since 𝑡1 , 𝑡2 ∈ adom(ℐ𝑀 −1 ) by assumption, the induction hypothesis on 𝐷 yields S0 (𝑡1 , 𝑡2 ) ∈ ℐ𝑀 |𝑀 −1 . Using Lemma 20, we thus obtain S0 (𝑡1 , 𝑡2 ) ∈ ℐ𝑀 −1 . Therefore 𝑅S is already applicable on ℐ𝑀 −1 and thus S(𝑡1 , 𝑡2 ) ∈ ℐ𝑀 as desired. 𝑅R,𝑖 . We have P(𝑡1 , . . . , 𝑡𝑚 ) = R𝑖+1 (𝑡1 , 𝑡2 ) and there exists some 𝑡 such that R𝑖 (𝑡1 , 𝑡) and S(𝑡, 𝑡2 ) have already been derived. In particular, R𝑖 (𝑡1 , 𝑡), S(𝑡, 𝑡2 ) ∈ ℐ𝑛+1 . If 𝑡 ∈ adom(ℐ𝑀 −1 ) then we can conclude by applying the induction hypothesis for 𝐷 on both R𝑖 (𝑡1 , 𝑡) and S(𝑡, 𝑡2 ), which are thus already in ℐ𝑀 , which is closed under our Datalog rules, in particular under 𝑅R,𝑖 , thus R𝑖+1 (𝑡1 , 𝑡2 ) ∈ ℐ𝑀 . We now focus on the case of 𝑡∈ / adom(ℐ𝑀 −1 ) and apply Corollary 25, recalling that S(𝑡, 𝑡2 ) and 𝑡2 ∈ adom(ℐ𝑀 −1 ) to obtain 𝑡 ∈ adom(ℐ𝑀 ). In particular, S(𝑡, 𝑡2 ) ∈ ℐ𝑀 by Lemma 20. We now distinguish two cases depending on whether R𝑖 (𝑡1 , 𝑡) ∈ ℐ𝑀 or not. If R𝑖 (𝑡1 , 𝑡) ∈ ℐ𝑀 , then closure under Datalog rules of ℐ𝑀 concludes as 𝑅R,𝑖 is already applicable in ℐ𝑀 . Otherwise R𝑖 (𝑡1 , 𝑡) ∈ / ℐ𝑀 and we can apply Lemma 21 to obtain either 𝑡1 ∈ adom(ℐ𝑀 ) ∖ adom(ℐ𝑀 −1 ) or Flood(𝑡1 ) ∈ ℐ𝑀 . The former is a contradiction with our assumption that 𝑡1 ∈ adom(ℐ𝑀 −1 ). The gen latter means that 𝑅flood triggers already in ℐ𝑀 for 𝑥 = 𝑡1 and 𝑦 = 𝑧 = 𝑡2 (since Flood(𝑡2 ) ∈ ℐ𝑀 follows from S(𝑡, 𝑡2 ) ∈ ℐ𝑀 ), thus introducing atom R𝑖+1 (𝑡1 , 𝑡2 ) ∈ ℐ𝑀 as desired. 𝑅T,𝑖 . The argument is essentially the same as for 𝑅 = 𝑅R,𝑖 . We have P(𝑡1 , . . . , 𝑡𝑚 ) = T𝑖 (𝑡1 , 𝑡2 , 𝑡3 ) and there exists some terms 𝑠, 𝑠′ such that T𝑖 (𝑡1 , 𝑠, 𝑠′ ), S𝑞𝑖 (𝑠, 𝑡2 ) and S𝑟𝑖 (𝑠′ , 𝑡3 ) have already been derived. In particular T𝑖 (𝑡1 , 𝑠, 𝑠′ ), S𝑞𝑖 (𝑠, 𝑡2 ), S𝑟𝑖 (𝑠′ , 𝑡3 ) ∈ ℐ𝑛+1 . If 𝑠, 𝑠′ ∈ adom(ℐ𝑀 −1 ) then we can again conclude using the induction hypothesis, proving that Rule 𝑅T,𝑖 was already applicable in ℐ𝑀 . Otherwise, using S𝑞𝑖 (𝑠, 𝑡2 ), S𝑟𝑖 (𝑠′ , 𝑡3 ) ∈ ℐ𝑛+1 , we have two terms 𝑢, 𝑢′ such that S(𝑢, 𝑡2 ), S(𝑢′ , 𝑡3 ) ∈ ℐ𝑛+1 . We use Corollary 25 to obtain 𝑢, 𝑢′ ∈ adom(ℐ𝑀 ), recalling that 𝑡2 , 𝑡3 ∈ adom(ℐ𝑀 −1 ). We now distinguish two cases depending on whether T𝑖 (𝑡1 , 𝑠, 𝑠′ ) ∈ ℐ𝑀 or not. If T𝑖 (𝑡1 , 𝑠, 𝑠′ ) ∈ ℐ𝑀 , then closure under Datalog rules of ℐ𝑀 concludes as 𝑅T,𝑖 is already applicable in ℐ𝑀 . Otherwise T𝑖 (𝑡1 , 𝑠, 𝑠′ ) ∈ / ℐ𝑀 and we can apply Lemma 21 to obtain either 𝑡1 ∈ adom(ℐ𝑀 ) ∖ adom(ℐ𝑀 −1 ) or Flood(𝑡1 ) ∈ ℐ𝑀 . The former is a contradiction with our assumption that 𝑡1 ∈ adom(ℐ𝑀 −1 ). The gen latter means that 𝑅flood triggers already in ℐ𝑀 for
𝑥 = 𝑡1 and 𝑦 = 𝑡2 and 𝑧 = 𝑡3 , thus introducing atom T𝑖+1 (𝑡1 , 𝑡2 , 𝑡3 ) ∈ ℐ𝑀 as desired. prop 𝑅flood . We have P(𝑡1 , . . . , 𝑡𝑚 ) = Flood(𝑡1 ) and there exists a term 𝑡 such that S(𝑡, 𝑡1 ) has already been derived. From 𝑡1 ∈ adom(ℐ𝑀 −1 ), applying Corollary 25 yields 𝑡 ∈ adom(ℐ𝑀 ). Then closure under Datalog rules of ℐ𝑀 guarantees Flood(𝑡1 ) ∈ ℐ𝑀 as 𝑅R,𝑖 is already applicable in ℐ𝑀 and we are done.
𝑅SEnd . We have P(𝑡1 , . . . , 𝑡𝑚 ) = S(𝑡1 , 𝑡1 ) and End(𝑡1 ). Since End(𝑡1 ) cannot be obtained by any rule, we have End(𝑡1 ) ∈ ℐ, thus End(𝑡1 ) ∈ ℐ𝑀 as desired. 𝑅Ginit . We have P(𝑡1 , . . . , 𝑡𝑚 ) = G(𝑡1 , 𝑡2 ) and there exists a term 𝑡 such that S(𝑡1 , 𝑡) and S(𝑡, 𝑡2 ) have already been derived. Since we have 𝑡1 ∈ adom(ℐ𝑀 −1 ) and S(𝑡1 , 𝑡) ∈ ℐ𝑛+1 , using Lemma 20 we get 𝑡 ∈ adom(ℐ𝑀 −1 ). We can thus use the induction hypothesis on both S(𝑡1 , 𝑡) and S(𝑡, 𝑡2 ), that thus both belong to ℐ𝑀 . Since ℐ𝑀 is closed under our Datalog rules, in particular under 𝑅Ginit , we obtain G(𝑡1 , 𝑡2 ) ∈ ℐ𝑀 as desired. step 𝑅G,𝑖 . We have P(𝑡1 , . . . , 𝑡𝑚 ) = G(𝑡1 , 𝑡2 ) and we have atoms G(𝑡1 , 𝑡), R𝑖 (𝑡1 , 𝑡) and T𝑖 (𝑡1 , 𝑡, 𝑡2 ) that have already been derived. We consider the smallest 𝑗 ≤ 𝑛 + 1 such that T𝑖 (𝑡1 , 𝑡, 𝑡2 ) ∈ ℐ𝑗+1 ∖ ℐ𝑗 and apply Lemma 21 on that fact. If we have some 𝑘 ≥ 0 such that S𝑘 (𝑡1 , 𝑡) ∈ ℐ𝑗 , then, joint with Lemma 20 it guarantees 𝑡 ∈ adom(ℐ𝑀 −1 ). We can thus apply the induction hypothesis on all three atoms G(𝑡1 , 𝑡), R𝑖 (𝑡1 , 𝑡) and T𝑖 (𝑡1 , 𝑡, 𝑡2 ) and conclude with closure of ℐ𝑀 under our Datalog rules. Otherwise we have Flood(𝑡1 ), Flood(𝑡2 ) ∈ ℐ𝑗 ⊆ ℐ𝑛+1 . Since 𝑡1 , 𝑡2 ∈ / adom(ℐ𝑛+1 ) ∖ adom(ℐ𝑛 ) as 𝑛 + 1 > 𝑀 and 𝑡1 , 𝑡2 ∈ adom(ℐ𝑀 −1 ), we have Flood(𝑡1 ), Flood(𝑡2 ) ∈ ℐ𝑛 . Therefore, by induction hypothesis on 𝑛, we have Flood(𝑡1 ), Flood(𝑡2 ) ∈ ℐ𝑀 . We use closure of ℐ𝑀 under Datalog rules to derive gen gen body of 𝑅flood guarantees that 𝑅flood . The Flood(𝑡1 ), . . . , Flood(𝑡𝑚 ) have all already been derived. Thus by induction hypothesis we have Flood(𝑡1 ), . . . , Flood(𝑡𝑚 ) ∈ ℐ𝑀 . Closure of ℐ𝑀 under Datalog rules then concludes.
𝑅∃ . All atoms in the head of 𝑅∃ features the freshly introduced element. But since 𝑛 > 𝑀 −1 and that all 𝑡𝑖 ’s belong to adom(ℐ𝑀 −1 ), the atom P(𝑡1 , . . . , 𝑡𝑚 ) cannot possibly have been introduced by 𝑅∃ .