The Chase in Lean - Crafting a Formal Library for Existential Rule Research
From International Center for Computational Logic
The Chase in Lean - Crafting a Formal Library for Existential Rule Research
Talk by Lukas Gerlach
- Location: APB-2026
- Start: 30. July 2026 at 11:00 am
- End: 30. July 2026 at 12:00 pm
- Research group: Knowledge-Based Systems
- Event series: Research Seminar Logic and AI
- iCal
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). This talk will present an endeavor of crafting a Lean framework around existential rules and the chase. It will 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, it will 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, it will 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.
Talk also presented at the KR conference, in Lisbon, 2026.
