Verifying Datalog reasoning with Lean

DOI10.4230/LIPICS.ITP.2025.36MaRDI QIDQ7323697zbMATH OpenFDO

Authors Johannes Tantow, Lukas Gerlach, Stephan Mennicke, Markus Krötzsch

Publication date 1 September 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.ITP.2025.36

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A certificate-based approach to formally verified approximations
• A Certified Distributed Security Logic for Authorizing Code
• Certified Graph View Maintenance with Regular Datalog
• Certifying algorithms
• Certifying higher-order polynomial interpretations
• Certifying standard and stratified Datalog inference engines in SSReflect
• Efficient, verified checking of propositional proofs
• scientific article; zbMATH DE number 2080480 (Why is no real title available?)
• scientific article; zbMATH DE number 7699423 (Why is no real title available?)
• Introduction to algorithms.
• Multi-shot ASP solving with clingo
• The challenge of computer mathematics
• The incredible ELK. From polynomial procedures to efficient reasoning with \(\mathcal {EL}\) ontologies
• The Lean 4 theorem prover and programming language
• Tuple-generating dependencies capture complex values
• Verifying a sequent calculus prover for first-order logic with functions in Isabelle/HOL

This page was built for publication: Verifying Datalog reasoning with Lean

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7323697)