Fighting my Proof Anxiety with Lean - The Restricted Chase Indeed Yields Universal Models
From International Center for Computational Logic
Fighting my Proof Anxiety with Lean - The Restricted Chase Indeed Yields Universal Models
Talk by Lukas Gerlach
- Location: APB 3027
- Start: 18. April 2024 at 11:00 am
- End: 18. April 2024 at 12:00 pm
- Research group: Knowledge-Based Systems
- Event series: Research Seminar Logic and AI
- iCal
The restricted chase is a fundamental reasoning algorithm in database theory that can be used for (conjunctive) query answering. For a given pair of a set of existential rules and a database, the restricted chase yields a so-called universal model. Such a model can be embedded into every (other) model and therefore be used for query answering.
We present a formalization of the restricted chase in the interactive theorem proving language "Lean" including a (well-known) proof that the chase indeed yields a universal model. We shine a light on key parts of the formalization and discuss lessons learned in the process.
- More info at: https://github.com/monsterkrampe/proof-library