arxiv: 2605.12349 · v1 · submitted 2026-05-12 · 💻 cs.DB

Recognition: no theorem link

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

Lucas Larroque , Quentin Mani\`ere

Authors on Pith no claims yet

Pith reviewed 2026-05-13 02:49 UTC · model grok-4.3

classification 💻 cs.DB

keywords existential ruleschase terminationbounded treewidthconjunctive query entailmentdecidabilityundecidabilityknowledge bases

0 comments

The pith

It remains undecidable whether existential rules belong to chase-termination classes or the bounded treewidth set even when conjunctive query entailment is decidable.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that membership in several prominent abstract classes of existential rules stays undecidable even after restricting the input to rule sets for which conjunctive query entailment is already known to be decidable. These classes include those defined by termination of the standard, restricted, and core chase procedures as well as the bounded treewidth set class. The result matters because the classes were introduced precisely to guarantee that basic reasoning tasks on knowledge bases remain computable, yet without a decision procedure for membership their theoretical guarantees cannot be applied in practice. The authors reach the negative answer by constructing reductions from undecidable problems that preserve both the failure of chase termination or bounded treewidth and the decidability of query entailment.

Core claim

Within any class of existential rules for which conjunctive query entailment is decidable, it remains undecidable to determine whether a given set of rules belongs to the classes on which every classical chase variant terminates or to the bounded treewidth set class.

What carries the argument

Reductions from undecidable problems that preserve both non-membership in the target abstract classes and the property that conjunctive query entailment remains decidable.

Load-bearing premise

The reductions used to prove undecidability can be carried out while preserving membership in a class that already guarantees decidable conjunctive query entailment.

What would settle it

An algorithm that takes a set of existential rules for which conjunctive query entailment is decidable and correctly decides whether the chase terminates on all instances would falsify the claim for the chase-based classes.

Figures

Figures reproduced from arXiv: 2605.12349 by Lucas Larroque, Quentin Mani\`ere.

**Figure 1.** 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 function defined as 𝑔(𝑛) = 𝑞𝑛 mod 𝑝 𝑟𝑛 mod 𝑝 · 𝑛. Then, next(𝐶) is defined if and only if 𝑔(enc(𝐶)) ̸= enc(𝐶), and in that case enc(next(𝐶)) = 𝑔(enc(𝐶)). Let 𝒢 = { 𝑔 𝑖 (2) | 𝑖 ∈ N }. Si… view at source ↗

**Figure 2.** Figure 2: Representation of predicates S0, End and atoms with shape T𝑖(𝑡0, _, _) in ChX 5 (ℐE) for some 𝑖 such that 𝑟𝑖 𝑞𝑖 = 2 3 . 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) (no… view at source ↗

**Figure 3.** 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 ℎ ′ : 𝑞 → ℐ𝑀 a… view at source ↗

read the original 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 bounded treewidth set (BTS) class.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Decidable CQ entailment does not make chase termination or BTS membership decidable, shown via reductions that the paper claims stay inside suitable classes.

read the letter

The main thing to know is that the paper gives a negative answer: even inside classes of existential rules where conjunctive query entailment is decidable, it is still undecidable whether the chase terminates for the usual variants or whether the rules belong to the bounded treewidth set. It reaches this by reductions from known undecidable problems, and the abstract presents this as settling a question left open in the cited literature. The work is useful because it draws a clean line between the properties we can decide and the meta-properties that stay out of reach, which matters for anyone building systems that rely on these abstract classes. The reductions themselves are the core technical contribution, and if they succeed in preserving membership in a decidable-CQ fragment, the result is solid. The potential soft spot is exactly whether the constructed rule sets remain inside such a fragment. The abstract gives no details on the syntactic restrictions used to enforce this, so the claim rests on the reductions not introducing unguarded cycles or other features that would make entailment undecidable. If the full proofs use something like guarded rules or another known decidable subclass and keep the image inside it, the argument holds; otherwise the result applies only to the unrestricted case. The paper does not appear to have circular definitions or self-referential fitting. This is for readers already working in existential rules, chase termination, and decidability boundaries in knowledge bases. They will see the value in having this separation made explicit. It deserves peer review because the question is well-posed and the reduction approach is the right tool for it, even if the details of the preservation step will need referee scrutiny.

Referee Report

1 major / 0 minor

Summary. The paper asks whether membership in abstract classes of existential rules (chase-terminating variants and the bounded treewidth set) becomes decidable when the rule sets are restricted to those for which conjunctive query entailment is already known to be decidable. It answers negatively, establishing undecidability results via reductions from known undecidable problems while claiming to preserve the CQ-decidability restriction.

Significance. If the reductions correctly preserve membership in a CQ-decidable class, the result is significant: it shows that the meta-properties guaranteeing decidable reasoning remain undecidable even inside the decidable fragment, sharpening the boundary between abstract and concrete classes of existential rules and informing the design of practical syntactic restrictions in database and knowledge-representation systems.

major comments (1)

[Reduction construction (throughout the proofs of the negative results)] The central reductions (from halting or similar undecidable problems to chase non-termination or non-BTS membership) must map into rule sets that lie inside some class C already known to have decidable CQ entailment. The manuscript should explicitly identify the syntactic or semantic restrictions used to enforce this membership and prove that the constructed rule sets satisfy them (e.g., by avoiding unguarded cycles or unbounded treewidth that would render CQ entailment undecidable). Without this verification, the reduction only establishes undecidability in the unrestricted case rather than inside the targeted restricted classes.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful review and for emphasizing the need to rigorously verify that our reductions remain inside CQ-decidable classes. We address the concern directly below and will revise the manuscript to make the preservation arguments fully explicit.

read point-by-point responses

Referee: [Reduction construction (throughout the proofs of the negative results)] The central reductions (from halting or similar undecidable problems to chase non-termination or non-BTS membership) must map into rule sets that lie inside some class C already known to have decidable CQ entailment. The manuscript should explicitly identify the syntactic or semantic restrictions used to enforce this membership and prove that the constructed rule sets satisfy them (e.g., by avoiding unguarded cycles or unbounded treewidth that would render CQ entailment undecidable). Without this verification, the reduction only establishes undecidability in the unrestricted case rather than inside the targeted restricted classes.

Authors: We agree that explicit verification is required. Each reduction in the paper is constructed so that the resulting rule sets belong to a concrete CQ-decidable class (specifically, the class of linear existential rules for the chase-termination results and the class of guarded rules with acyclic dependency graphs for the BTS results). These classes are known to admit decidable CQ entailment via existing results in the literature. The constructions deliberately avoid unguarded cycles, ensure the rule dependency graph remains acyclic, and produce only rules whose associated hypergraphs have bounded treewidth. To make this fully rigorous, we will add a new subsection (or appendix) in the revised version that, for each theorem, (i) recalls the precise syntactic definition of the target CQ-decidable class, (ii) states the invariant maintained by the reduction, and (iii) proves by induction on the construction that every generated rule set satisfies the invariant. This will confirm that the undecidability statements hold inside the restricted classes rather than only in the unrestricted setting. revision: yes

Circularity Check

0 steps flagged

No significant circularity in undecidability reduction

full rationale

The paper establishes undecidability results for membership in chase-termination classes and the BTS class, restricted to settings where CQ entailment remains decidable, via reductions from known undecidable problems. No self-definitional steps, fitted inputs renamed as predictions, or load-bearing self-citations appear in the abstract or described derivation chain. The central claim rests on external reductions that are independent of the target property, making the proof self-contained without circular reduction to its own inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The result rests on standard undecidability reductions from the general existential-rules setting together with the assumption that those reductions can be performed inside classes that already guarantee decidable CQ entailment.

axioms (1)

standard math Chase termination and BTS membership are undecidable in the unrestricted existential-rules setting
Used as the source problem for the reduction that preserves CQ decidability.

pith-pipeline@v0.9.0 · 5461 in / 1097 out tokens · 66167 ms · 2026-05-13T02:49:35.715962+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

23 extracted references · 23 canonical work pages

[1]

Kolaitis

[Afrati and Kolaitis, 2008] Foto Afrati and Phokion G. Kolaitis. Answering aggregate queries in data exchange. InProceedings of the 27th ACM SIGMOD-SIGACT- SIGART Symposium on Principles of Database Sys- tems, PODS’08, page 129–138. Association for Com- puting Machinery,

work page 2008
[2]

Extending de- cidable cases for rules with existential variables

[Bagetet al., 2009] Jean-François Baget, Michel Leclère, Marie-Laure Mugnier, and Êric Salvat. Extending de- cidable cases for rules with existential variables. In Proceedings of the 21st International Joint Confer- ence on Artificial Intelligence, IJCAI’09, page 677–682. Morgan Kaufmann Publishers Inc.,

work page 2009
[3]

[Beeri and Vardi, 1981] Catriel Beeri and Moshe Y. Vardi. The implication problem for data dependencies. InProceedings of the 8th Colloquium on Automata, Languages and Programming, ICALP’81, page 73–85. Springer-Verlag,

work page 1981
[4]

Oblivious chase termination: The sticky case

[Calautti and Pieris, 2019] Marco Calautti and Andreas Pieris. Oblivious chase termination: The sticky case. InProceedings of the 22nd International Conference on Database Theory, ICDT’19, pages 17:1–17:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik,

work page 2019
[5]

Chase termination for guarded existential rules

[Calauttiet al., 2015] Marco Calautti, Georg Gottlob, and Andreas Pieris. Chase termination for guarded existential rules. InProceedings of the 34th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS’15, page 91–103. Association for Computing Machinery,

work page 2015
[6]

Taming the infinite chase: Query an- sweringunderexpressiverelationalconstraints.J

[Calìet al., 2013] Andrea Calì, Georg Gottlob, and Michael Kifer. Taming the infinite chase: Query an- sweringunderexpressiverelationalconstraints.J. Artif. Intell. Res., 48:115–174,

work page 2013
[7]

A general datalog-based frame- work for tractable query answering over ontologies

[Calìet al., 2012] Andrea Calì, Georg Gottlob, and Thomas Lukasiewicz. A general datalog-based frame- work for tractable query answering over ontologies. Journal of Web Semantics, 14:57–83,

work page 2012
[8]

[Carralet al., 2022] David Carral, Lucas Larroque, Marie-Laure Mugnier, and Michaël Thomazo. Nor- malisations 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,

work page 2022
[9]

The monadic second- order logic of graphs

[Courcelle, 1990] Bruno Courcelle. The monadic second- order logic of graphs. I. recognizable sets of finite graphs.Inf. Comput., 85(1):12–75,

work page 1990
[10]

Characterizing boundedness in chase variants.Theory Pract

[Delivoriaset 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,

work page 2021
[11]

The chase revisited

[Deutschet al., 2008] Alin Deutsch, Alan Nash, and Jeff Remmel. The chase revisited. InProceedings of the 27th ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS’08, page 149–158. Association for Computing Machinery,

work page 2008
[12]

Tuple-generating dependen- cies

[Fagin, 2018] Ronald Fagin. Tuple-generating dependen- cies. InEncyclopedia of Database Systems, Second Edition. Springer,

work page 2018
[13]

Answer counting under guarded tgds.Log

[Feieret al., 2023] Cristina Feier, Carsten Lutz, and Marcin Przybylko. Answer counting under guarded tgds.Log. Methods Comput. Sci., 19(3),

work page 2023
[14]

Mairson, Yehoshua Sagiv, and Moshe Y

[Gaifmanet 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,

work page 1993
[15]

About the multi-head linear restricted chase termina- tion

[Gerlachet al., 2025] Lukas Gerlach, Lucas Larroque, Jerzy Marcinkowski, and Piotr Ostropolski-Nalewaja. About the multi-head linear restricted chase termina- tion. InProceedings of the 22nd International Confer- ence on Principles of Knowledge Representation and Reasoning, KR’25, pages 346–355,

work page 2025
[16]

All-instances termination of chase is undecidable

[Gogacz and Marcinkowski, 2014] Tomasz Gogacz and Jerzy Marcinkowski. All-instances termination of chase is undecidable. InProceedings of the 41st International Colloquium on Automata, Languages, and Program- ming, ICALP’14, pages 293–304. Springer,

work page 2014
[17]

All-instances restricted chase termination

[Gogaczet al., 2020] Tomasz Gogacz, Jerzy Marcinkowski, and Andreas Pieris. All-instances restricted chase termination. InProceedings of the 39th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS’20, page 245–258. Association for Computing Machinery,

work page 2020
[18]

Computing universal models under guarded tgds

[Hernich, 2012] André Hernich. Computing universal models under guarded tgds. InProceedings of the 15th International Conference on Database Theory, ICDT’12, page 222–235. Association for Computing Machinery,

work page 2012
[19]

Mendelzon, and Yehoshua Sagiv

[Maieret al., 1979] David Maier, Alberto O. Mendelzon, and Yehoshua Sagiv. Testing implications of data de- pendencies.ACM Trans. Database Syst., 4(4):455–469,

work page 1979
[20]

Generalized schema- mappings: from termination to tractability

[Marnette, 2009] Bruno Marnette. Generalized schema- mappings: from termination to tractability. In Proceedings of the 28th ACM SIGMOD-SIGACT- SIGART Symposium on Principles of Database Sys- tems, PODS’09, page 13–22. Association for Comput- ing Machinery,

work page 2009
[21]

Minsky.Computation: Finite and Infinite Machines

[Minsky, 1967] Marvin L. Minsky.Computation: Finite and Infinite Machines. Prentice-Hall,

work page 1967
[22]

Stream reasoning in temporal datalog

[Roncaet al., 2018] Alessandro Ronca, Mark Kaminski, Bernardo Cuenca Grau, Boris Motik, and Ian Horrocks. Stream reasoning in temporal datalog. InProceedings of the 32nd AAAI Conference on Artificial Intelligence, AAAI’18, pages 1941–1948. AAAI Press,

work page 2018
[23]

Then, sinceEnd(𝑤)∈ ChX 𝑛+1(ℐE), Rule𝑅∃is applicable onChX 𝑛+1(ℐE)by map- ping 𝑦to 𝑡𝑔𝑘(2)

Hence, by Item (iii) of Lemma 13, G(𝑡0,𝑤)∈ChX 𝑛+1(ℐE). Then, sinceEnd(𝑤)∈ ChX 𝑛+1(ℐE), Rule𝑅∃is applicable onChX 𝑛+1(ℐE)by map- ping 𝑦to 𝑡𝑔𝑘(2). Since by construction, theS0-atoms of ChX 𝑛+1(ℐE)are exactly{S0(𝑡𝑖,𝑡𝑖+1)|0≤𝑖<𝑛}, there is no way to homomorphically map the result of applying 𝑅∃intoCh X 𝑛+1(ℐE), so the rule is indeedE-applicable. Thus, this pro...

work page 2008