Inproceedings3417

r Informatik |Editor=Yannick Forster, Chantal Keller |Series=LIPIcs |Volume=352 }}

PublikationenPublications

• Nach AutorBy Author
  • Lukas GerlachLukas Gerlach
  • Stephan MennickeStephan Mennicke
  • Markus KrötzschMarkus Krötzsch
• Nach ForschungsgruppeBy Research Group
  • Wissensbasierte SystemeKnowledge-Based Systems

Toggle side column

Verifying Datalog Reasoning with Lean

Johannes TantowJohannes Tantow,  Lukas GerlachLukas Gerlach,  Stephan MennickeStephan Mennicke,  Markus KrötzschMarkus Krötzsch

• Download

Johannes Tantow, Lukas Gerlach, Stephan Mennicke, Markus Krötzsch
Verifying Datalog Reasoning with Lean
16th Conference on Interactive Theorem Proving (ITP 2025), to appear. Schloss Dagstuhl - Leibniz-Zentrum f{\"{u

• Details
• Bibtex

• KurzfassungAbstract
  Datalog is an essential logical rule language with many applications, and modern rule engines compute logical consequences for Datalog with high performance and scalability. While Datalog is rather simple and, in principle, explainable by design, such sophisticated implementations and optimizations are hard to verify. We therefore propose a certificate-based approach to validate results of Datalog reasoners in a formally verified checker for Datalog proofs. Using the proof assistant Lean, we implement such a checker and verify its correctness against direct formalizations of the Datalog semantics. We propose two JSON encodings for Datalog proofs: one using the widely supported Datalog proof trees, and one using directed acyclic graphs for succinctness. To evaluate the practical feasibility and performance of our approach, we validate proofs that we obtain by converting derivation traces of an existing Datalog reasoner into our tool-independent format.
• Weitere Informationen unter:Further Information: Link
• Projekt:Project: Cfaed, CPEC, CeTI, SECAI, ScaDS.AI
• Verknüpfte Tools:Related Tools: Nemo
• Forschungsgruppe:Research Group: Wissensbasierte SystemeKnowledge-Based Systems

@inproceedings{TGMK2025,
  author    = {Johannes Tantow and Lukas Gerlach and Stephan Mennicke and Markus
               Kr{\"{o}}tzsch},
  title     = {Verifying Datalog Reasoning with Lean},
  booktitle = {16th Conference on Interactive Theorem Proving (ITP 2025)},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u},
  year      = {2025},
  month     = {September}
}