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.

翻译：追逐是一种用于存在规则（即元组生成依赖）推理的可靠、完备但可能非终止的算法，该规则是一种高表达性的知识表示语言。尽管该过程看似简单，但关于其理论性质及实际实现优化的研究已发展到难以验证正确性和复现证明的地步，且直觉有时可能具有误导性。Lean是一种纯函数式编程语言及交互式定理证明器，其社区正积极开发数学（Mathlib）和计算机科学（CSLib）形式化库。在本工作中，我们介绍了围绕存在规则与追逐构建Lean框架的尝试。我们讨论了关于文献中常见追逐定义细微差别的设计决策，并展示了这些定义如何转化为Lean代码。为通过已知结果说明框架的能力，我们证明了追逐的结果是通用模型，并概述了证明过程：在没有所谓"替代匹配"的情况下，该结果甚至是一个核心模型。在现有文献基础上，我们将类似模型忠实无环性（MFA）的追逐终止充分条件统一到一个通用框架中，同时增加了对规则中常量的支持。