Fighting my Proof Anxiety with Lean - The Restricted Chase Indeed Yields Universal Models
Aus International Center for Computational Logic
Fighting my Proof Anxiety with Lean - The Restricted Chase Indeed Yields Universal Models
Vortrag von Lukas Gerlach
- Veranstaltungsort: APB 3027
- Beginn: 18. April 2024 um 11:00
- Ende: 18. April 2024 um 12:00
- Forschungsgruppe: Wissensbasierte Systeme
- 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.
- Weitere Infos unter: https://github.com/monsterkrampe/proof-library
