pith. sign in

arxiv: 2604.22531 · v1 · submitted 2026-04-24 · 💻 cs.LO · cs.DB

The Chase in Lean -- Crafting a Formal Library for Existential Rule Research

Lukas Gerlach This is my paper

Pith reviewed 2026-05-08 09:43 UTC · model grok-4.3

classification 💻 cs.LO cs.DB
keywords existential ruleschase procedureuniversal modelcore modeltermination conditionsformal librarytuple-generating dependenciesknowledge representation
0
0 comments X

The pith

Formal library proves the chase yields a universal model for existential rules.

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

The paper builds a formal framework to define the chase procedure for existential rules and verify its properties. It establishes that the output of the chase is a universal model, which satisfies the rules and serves as a canonical structure that any other model can map into. The framework also unifies various sufficient conditions for the chase to terminate, extending them to handle constants in the rules. A reader would care because informal reasoning about the chase can be tricky due to its potential non-termination and varying definitions, making formal verification valuable for reliable knowledge representation and reasoning systems.

Core claim

In the formalized library, the result of applying the chase to a set of existential rules is shown to be a universal model. The formalization outlines how, in the absence of alternative matches, this model qualifies as a core. Additionally, the work unifies chase termination conditions similar to model-faithful acyclicity into a single framework and incorporates support for constants within the rules.

What carries the argument

The formal definitions and proofs for the chase procedure, including the handling of alternative matches, which enable the establishment of universality and core properties.

If this is right

  • The universality result confirms that the chase can be used for complete reasoning in existential rule systems.
  • Unified termination conditions allow checking chase termination under a broader set of rule sets including those with constants.
  • The outline for proving the core property supports further formal analysis of minimality in models.
  • Design decisions on chase variants clarify nuances that affect correctness in implementations.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • This approach could facilitate the formal verification of optimizations for the chase algorithm.
  • It provides a basis for comparing and reconciling different definitions of the chase across research papers.
  • Future work might extend the library to prove properties of query answering over existential rules.

Load-bearing premise

The formal encodings of the chase variants and alternative matches match the informal definitions and handle all edge cases from the literature correctly.

What would settle it

A concrete example of existential rules where the formalized chase result fails to be a universal model, such as not admitting a homomorphism from it to some other model that satisfies the rules.

read the original abstract

The chase is a sound, complete, but possibly non-terminating algorithm for reasoning with existential rules (aka. tuple-generating dependencies), a highly expressive knowledge representation language. Although the procedure appears simple, research on theoretical properties and optimization for practical implementations has grown to a point where verifying correctness and reproducing proofs becomes challenging and intuition can sometimes be misleading. Lean is a purely functional programming language and interactive theorem prover whose community actively develops formal libraries for mathematics (Mathlib) and computer science (CSLib). In this work, we present our own endeavor of crafting a Lean framework around existential rules and the chase. We discuss design decisions concerning the nuances of chase definitions commonly found in the literature and show how these translate into Lean. To illustrate the framework's capabilities using known results, we show that the result of a chase is a universal model and outline the formalization for proving that without so-called "alternative matches" it is even a core. Beyond existing literature, we unify sufficient chase termination conditions in the likeness of Model-Faithful Acyclicity (MFA) into a common framework while also adding support for constants in rules.

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.

Referee Report

2 major / 2 minor

Summary. The manuscript presents a Lean framework for existential rules and the chase procedure. It discusses design decisions for chase definitions from the literature, shows that the result of a chase is a universal model, outlines a formalization proving it is a core without alternative matches, unifies sufficient termination conditions in the style of Model-Faithful Acyclicity (MFA) into a common framework, and adds support for constants in rules.

Significance. If the encodings are faithful, the work supplies a machine-checked library that can verify core properties of the chase (universality, core-ness under restricted matches) and unify termination criteria. This is valuable in a field where informal proofs are error-prone and where implementations must be trusted for reasoning tasks.

major comments (2)
  1. The central universality and core claims rest on the Lean definitions of the chase step, match relation, null generation, and the 'alternative matches' predicate. The manuscript must explicitly compare these encodings to the variants in the literature (e.g., how multiple matches are resolved, interaction of constants with existentials, and detection of alternative matches) and state any discrepancies; without such a comparison the theorems do not necessarily transfer to the informal results they cite.
  2. The unification of MFA-style termination conditions is presented as a common framework. The manuscript should identify which specific conditions from the literature are recovered as special cases and prove that the unified criterion is at least as general as each original one; otherwise the claim of unification beyond existing literature is not substantiated.
minor comments (2)
  1. Clarify the precise statement of the 'outline the formalization' for the core property: is the full proof completed in Lean or only a high-level sketch?
  2. Provide a table or section listing the supported chase variants and the design choices made for each (e.g., oblivious vs. restricted vs. standard chase).

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive major comments. We address each point below and commit to revisions that strengthen the manuscript's connections to the literature without altering its core contributions.

read point-by-point responses

  1. Referee: The central universality and core claims rest on the Lean definitions of the chase step, match relation, null generation, and the 'alternative matches' predicate. The manuscript must explicitly compare these encodings to the variants in the literature (e.g., how multiple matches are resolved, interaction of constants with existentials, and detection of alternative matches) and state any discrepancies; without such a comparison the theorems do not necessarily transfer to the informal results they cite.

    Authors: We agree that an explicit side-by-side comparison would improve clarity and transferability. Section 3 already discusses our design choices for the chase step, match relation, and null generation, including how we handle multiple matches via a deterministic selection strategy and how constants interact with existentials through typed nulls. The alternative-matches predicate is defined to match the standard notion from the cited literature. In the revision we will add a new subsection (likely 3.4) that tabulates our encodings against the main variants (e.g., those in [standard references for chase semantics]), explicitly notes the resolution of multiple matches, the constant-existential interaction, and the detection of alternative matches, and states that the only discrepancy is a minor Lean-specific representation of nulls that does not affect the universality or core proofs. We will also add a short paragraph arguing why the formalized theorems therefore carry over to the informal results. revision: yes

  2. Referee: The unification of MFA-style termination conditions is presented as a common framework. The manuscript should identify which specific conditions from the literature are recovered as special cases and prove that the unified criterion is at least as general as each original one; otherwise the claim of unification beyond existing literature is not substantiated.

    Authors: We accept the need for explicit recovery statements and generality proofs. Our unified framework generalizes the acyclicity condition underlying MFA by parameterizing the dependency graph construction; MFA is recovered exactly when the parameter is set to the standard model-faithful instantiation. In the revision we will (i) list the concrete conditions recovered as special cases (MFA and the two main weakenings discussed in the MFA paper), (ii) add a lemma proving that each original condition implies our unified criterion, and (iii) include a short argument that the unified criterion is at least as general as each of them. These additions will be placed in the termination section and will not change the existing formalization. revision: yes

Circularity Check

0 steps flagged

Formalization of chase properties and MFA unification is self-contained machine-checked work

full rationale

The paper presents a new Lean library that encodes chase variants, alternative matches, and termination conditions, then formally proves that chase yields a universal model and outlines a core proof when alternative matches are disallowed. These are established informal results now machine-verified rather than derived from fitted parameters, self-referential equations, or load-bearing self-citations. The MFA-style unification is explicitly positioned as an extension beyond prior literature. No quoted step reduces by construction to its own inputs; the central claims rest on the independent formal development.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claims rest on standard Lean and Mathlib foundations for inductive definitions and theorem proving; no free parameters, ad-hoc axioms, or invented entities are introduced beyond the usual formalization choices for encoding rules and matches.

axioms (1)
  • standard math Standard Lean inductive types and dependent pattern matching suffice to encode existential rules and chase steps without loss of generality.
    Invoked when translating literature definitions of chase into Lean code.

pith-pipeline@v0.9.0 · 5490 in / 1309 out tokens · 56901 ms · 2026-05-08T09:43:42.623727+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

37 extracted references · 37 canonical work pages

  1. [1]

    write newline

    " write newline "" before.all 'output.state := FUNCTION fin.entry add.period write newline FUNCTION new.block output.state before.all = 'skip after.block 'output.state := if FUNCTION new.sentence output.state after.block = 'skip output.state before.all = 'skip after.sentence 'output.state := if if FUNCTION not #0 #1 if FUNCTION and 'skip pop #0 if FUNCTIO...

    work page

  2. [2]

    Abiteboul, S.; Hull, R.; and Vianu, V. 1995. Foundations of Databases . Addison-Wesley

    work page 1995

  3. [3]

    R.; Commelin, J.; Chen, B

    Baanen, A.; Ballard, M. R.; Commelin, J.; Chen, B. G.-g.; Rothgang, M.; and Testa, D. 2026. Growing mathlib: maintenance of a large scale mathematical library. In de Paiva, V., and Koepke, P., eds., Intelligent Computer Mathematics , 51--70. Cham: Springer Nature Switzerland

    work page 2026

  4. [4]

    Baget, J.; Lecl \` e re, M.; Mugnier, M.; and Salvat, E. 2011. On rules with existential variables: Walking the decidability line. Artif. Intell. 175(9-10):1620--1654

    work page 2011

  5. [5]

    Baget, J.; Garreau, F.; Mugnier, M.; and Rocher, S. 2014. Extending acyclicity notions for existential rules. In Schaub, T.; Friedrich, G.; and O'Sullivan, B., eds., ECAI 2014 - 21st European Conference on Artificial Intelligence , volume 263 of Frontiers in Artificial Intelligence and Applications , 39--44. IOS Press

    work page 2014

  6. [6]

    Barrett, C.; Chaudhuri, S.; Montesi, F.; Grundy, J.; Kohli, P.; de Moura, L.; Rademaker, A.; and Yingchareonthawornchai, S. 2026. Cslib: The lean computer science library

    work page 2026

  7. [7]

    Beeri, C., and Vardi, M. Y. 1984. A proof procedure for data dependencies. J. ACM 31(4):718--741

    work page 1984

  8. [8]

    Benzaken, V.; Contejean, E.; and Dumbrava, S. 2017. Certifying standard and stratified datalog inference engines in ssreflect. In Ayala - Rinc \' o n, M., and Mu \ n oz, C. A., eds., Interactive Theorem Proving - 8th International Conference, ITP , volume 10499 of Lecture Notes in Computer Science , 171--188. Springer

    work page 2017

  9. [9]

    Bonifati, A.; Dumbrava, S.; and Arias, E. J. G. 2018. Certified graph view maintenance with regular datalog. Theory Pract. Log. Program. 18(3-4):372--389

    work page 2018

  10. [10]

    Bourhis, P.; Manna, M.; Morak, M.; and Pieris, A. 2016. Guarded-based disjunctive tuple-generating dependencies. ACM Trans. Database Syst. 41(4):27:1--27:45

    work page 2016

  11. [11]

    Carral, D.; Larroque, L.; Mugnier, M.-L.; and Thomazo, M. 2022. Normalisations of Existential Rules: Not so Innocuous! In Proceedings of the 19th International Conference on Principles of Knowledge Representation and Reasoning , 102--111

    work page 2022

  12. [12]

    Carral, D.; Gerlach, L.; Larroque, L.; and Thomazo, M. 2025. Restricted chase termination: You want more than fairness. Proc. ACM Manag. Data 3(2 (PODS))

    work page 2025

  13. [13]

    Carral, D.; Dragoste, I.; and Kr \" o tzsch, M. 2017. Restricted chase (non)termination for existential rules with disjunctions. In Sierra, C., ed., Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017 , 922--928. ijcai.org

    work page 2017

  14. [14]

    Cuenca Grau , B.; Horrocks, I.; Kr \" o tzsch, M.; Kupke, C.; Magka, D.; Motik, B.; and Wang, Z. 2013. Acyclicity notions for existential rules and their application to query answering in ontologies. J. Artif. Intell. Res. 47:741--808

    work page 2013

  15. [15]

    de Moura, L., and Ullrich, S. 2021. The lean 4 theorem prover and programming language. In Platzer, A., and Sutcliffe, G., eds., CADE 28 - 28th International Conference on Automated Deduction , volume 12699 of Lecture Notes in Computer Science , 625--635. Springer

    work page 2021

  16. [16]

    Deutsch, A.; Nash, A.; and Remmel, J. B. 2008. The chase revisited. In Lenzerini, M., and Lembo, D., eds., Proceedings of the Twenty-Seventh ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS 2008 , 149--158. ACM

    work page 2008

  17. [17]

    Dumbrava, S. 2016. Formalisation en Coq de Bases de Donn \' e es Relationnelles et D \' e ductives -et M \' e canisation de Datalog. (A Coq Formalization of Relational and Deductive Databases -and a Mechanizations of Datalog) . Ph.D. Dissertation, University of Paris-Saclay, France

    work page 2016

  18. [18]

    G.; Miller, R

    Fagin, R.; Kolaitis, P. G.; Miller, R. J.; and Popa, L. 2005. Data exchange: semantics and query answering. Theor. Comput. Sci. 336(1):89--124

    work page 2005

  19. [19]

    Gerlach, L., and Carral, D. 2023a. Do repeat yourself: Understanding sufficient conditions for restricted chase non-termination. In Marquis, P.; Son, T. C.; and Kern - Isberner, G., eds., Proceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning, KR 2023 , 301--310

    work page 2023

  20. [20]

    Gerlach, L., and Carral, D. 2023b. General acyclicity and cyclicity notions for the disjunctive skolem chase. In Williams, B.; Chen, Y.; and Neville, J., eds., Thirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023 , 6372--6379. AAAI Press

    work page 2023

  21. [21]

    Gerlach, L.; Larroque, L.; Marcinkowski, J.; and Ostropolski-Nalewaja, P. 2025. About the Multi-Head Linear Restricted Chase Termination . In Proceedings of the 22nd International Conference on Principles of Knowledge Representation and Reasoning , 346--355

    work page 2025

  22. [22]

    Gogacz, T., and Marcinkowski, J. 2014. All-instances termination of chase is undecidable. In Esparza, J.; Fraigniaud, P.; Husfeldt, T.; and Koutsoupias, E., eds., Automata, Languages, and Programming - 41st International Colloquium, ICALP 2014 , volume 8573 of Lecture Notes in Computer Science , 293--304. Springer

    work page 2014

  23. [23]

    Gogacz, T.; Marcinkowski, J.; and Pieris, A. 2023. Uniform restricted chase termination. SIAM J. Comput. 52(3):641--683

    work page 2023

  24. [24]

    Grahne, G., and Onet, A. 2018. Anatomy of the chase. Fundam. Informaticae 157(3):221--270

    work page 2018

  25. [25]

    Hanisch, P., and Kr \" o tzsch, M. 2024. Chase termination beyond polynomial time. Proc. ACM Manag. Data 2(2):93

    work page 2024

  26. [26]

    Ivliev, A.; Gerlach, L.; Meusel, S.; Steinberg, J.; and Kr \" o tzsch, M. 2024. Nemo: Your friendly and versatile rule reasoning toolkit. In Marquis, P.; Ortiz, M.; and Pagnucco, M., eds., Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning, KR 2024

    work page 2024

  27. [27]

    Jordan, H.; Scholz, B.; and Subotic, P. 2016. Souffl \' e : On synthesis of program analyzers. In Chaudhuri, S., and Farzan, A., eds., Computer Aided Verification - 28th International Conference, CAV 2016 , volume 9780 of Lecture Notes in Computer Science , 422--430. Springer

    work page 2016

  28. [28]

    Karimi, A.; Zhang, H.; and You, J. 2021. Restricted chase termination for existential rules: A hierarchical approach and experimentation. Theory Pract. Log. Program. 21(1):4--50

    work page 2021

  29. [29]

    Kr \" o tzsch, M., and Rudolph, S. 2011. Extending decidable existential rules by joining acyclicity and guardedness. In Walsh, T., ed., IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence , 963--968. IJCAI/AAAI

    work page 2011

  30. [30]

    Kr \" o tzsch, M. 2020. Computing cores for existential rules with the standard chase and ASP . In Calvanese, D.; Erdem, E.; and Thielscher, M., eds., Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020 , 603--613

    work page 2020

  31. [31]

    Lecl\` e re, M.; Mugnier, M.-L.; Thomazo, M.; and Ulliana, F. 2019. A Single Approach to Decide Chase Termination on Linear Existential Rules . In Barcelo, P., and Calautti, M., eds., 22nd International Conference on Database Theory (ICDT 2019) , volume 127 of Leibniz International Proceedings in Informatics (LIPIcs) , 18:1--18:19. Dagstuhl, Germany: Schl...

    work page 2019

  32. [32]

    Marnette, B. 2009. Generalized schema-mappings: from termination to tractability. In Paredaens, J., and Su, J., eds., Proceedings of the Twenty-Eigth ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS 2009 , 13--22. ACM

    work page 2009

  33. [33]

    Nenov, Y.; Piro, R.; Motik, B.; Horrocks, I.; Wu, Z.; and Banerjee, J. 2015. Rdfox: A highly-scalable RDF store. In Arenas, M.; Corcho, \' O .; Simperl, E.; Strohmaier, M.; d'Aquin, M.; Srinivas, K.; Groth, P.; Dumontier, M.; Heflin, J.; Thirunarayan, K.; and Staab, S., eds., The Semantic Web - ISWC 2015 - 14th International Semantic Web Conference , volu...

    work page 2015

  34. [34]

    Schlichtkrull, A.; Rydhof Hansen, R.; and Nielson, F. 2024. Isabelle-verified correctness of datalog programs for program analysis. In Proceedings of the 39th ACM/SIGAPP Symposium on Applied Computing (SAC 2024) , 1731--1734. ACM

    work page 2024

  35. [35]

    Tantow, J.; Gerlach, L.; Mennicke, S.; and Kr \" o tzsch, M. 2025. Verifying datalog reasoning with Lean . In Forster, Y., and Keller, C., eds., Proceedings of the 16th International Conference on Interactive Theorem Proving (ITP'25) , volume 352 of LIPIcs . Dagstuhl Publishing

    work page 2025

  36. [36]

    Urbani, J.; Jacobs, C. J. H.; and Kr \" o tzsch, M. 2016. Column-oriented datalog materialization for large knowledge graphs. In Schuurmans, D., and Wellman, M. P., eds., Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence , 258--264. AAAI Press

    work page 2016

  37. [37]

    Whitehead, N. 2007. A certified distributed security logic for authorizing code. In Altenkirch, T., and McBride, C., eds., Types for Proofs and Programs , 253--268. Springer

    work page 2007