Will My Favorite Chases Terminate if Evaluating Conjunctive Queries Does? One Does Not Simply Decide This

Existential rules (also known as tuple-generating dependencies, TGDs) are a central formalism for enriching databases with domain knowledge. A knowledge base consists of a database $D$ and a set of existential rules $\Sigma$; reasoning amounts to querying the finite or infinite universal model obtained by applying the chase procedure. However, reasoning with arbitrary existential rules is undecidable, even for basic tasks such as conjunctive query (CQ) entailment. To regain decidability, the community has identified numerous classes of rules with useful properties. One prominent family consists of rule sets on which the chase algorithm always terminates, guaranteeing a finite universal model. Another is the bounded treewidth set (BTS) class, which ensures that the chase has bounded treewidth and thus supports decidable CQ entailment. A recurring problem is that these classes are often *abstract*: given a set of rules, it may be undecidable to check whether it belongs to the class. Since the most studied classes of existential rules are designed for database reasoning and guarantee decidable CQ entailment, the authors ask a natural question: within a class that supports decidable query entailment, do the usual abstract classes become concrete? In other words, if we restrict attention to rule sets for which CQ entailment is decidable, can we decide whether the chase terminates (for various variants) or whether the set is BTS? This paper answers this question in the negative.

The authors conduct a decidability analysis of membership problems for chase-termination classes and the BTS class, under the assumption that the ambient class already enjoys decidable conjunctive query entailment. The study covers all classical chase variants: the oblivious chase, the semi-oblivious chase, the restricted chase, and the core chase. For each variant, the termination problem asks whether, for a given finite set of existential rules $\Sigma$, the chase terminates on every database $D$ (or on a given database). The BTS membership problem asks whether the set of rules is a bounded treewidth set. The technical approach reduces from known undecidable problems, such as the halting problem for Turing machines or the Post correspondence problem, by encoding computations into rule sets that remain within a decidable CQ-entailment class. The reductions are carefully designed so that the resulting rule sets satisfy the conditions of the ambient class (e.g., guardedness or weak acyclicity) while simulating the undecidable behavior. This establishes that even under the promise of decidable CQ entailment, the membership problems remain undecidable. The paper also clarifies the relationships between the different chase variants and the BTS class in this restricted setting.