Document Open Access Logo

Verifying Datalog Reasoning with Lean

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

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.ITP.2025.36.pdf
  • Filesize: 0.99 MB
  • 19 pages
HTML5 Logo HTML (experimental)
LIPIcs.ITP.2025.36.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
  • Computing methodologies → Theorem proving algorithms
  • Theory of computation → Constraint and logic programming
  • Theory of computation → Automated reasoning
Keywords
  • Certifying Algorithms
  • Datalog
  • Formal Verification

Metrics

Abstract

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.

Cite As Get BibTex

Johannes Tantow, Lukas Gerlach, Stephan Mennicke, and Markus Krötzsch. Verifying Datalog Reasoning with Lean. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 36:1-36:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ITP.2025.36

Author Details

Johannes Tantow
  • TU Chemnitz, Germany
Lukas Gerlach
  • Knowledge-Based Systems Group, TU Dresden, Germany
Stephan Mennicke
  • Knowledge-Based Systems Group, TU Dresden, Germany
Markus Krötzsch
  • Knowledge-Based Systems Group, TU Dresden, Germany

Funding

This work was partly supported by DFG (German Research Foundation) in project 389792660 (TRR 248, https://www.perspicuous-computing.science/) and in the CeTI Cluster of Excellence; by the Bundesministerium für Bildung und Forschung (BMBF) in the https://www.scads.de (ScaDS.AI) and in project 13GW0552B (https://digitalhealth.tu-dresden.de/projects/kimeds/); by BMBF and DAAD (German Academic Exchange Service) in project 57616814 (https://secai.org/, https://secai.org/); and by the https://cfaed.tu-dresden.de (cfaed).

Acknowledgements

We would like to thank Markus Himmel for his help and useful feedback during the integration of our results on hash maps into the standard library.

Supplementary Materials

References

  1. Serge Abiteboul, Richard Hull, and Victor Vianu. Foundations of Databases. Addison Wesley, 1994. Google Scholar
  2. Eyad Alkassar, Sascha Böhme, Kurt Mehlhorn, and Christine Rizkallah. Verification of certifying computations. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification - 23rd Int. Conf. CAV'11, volume 6806 of LNCS, pages 67-82. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22110-1_7.
  3. Franz Baader, Patrick Koopmann, and Cesare Tinelli. First results on how to certify subsumptions computed by the EL reasoner ELK using the logical framework with side conditions. In Stefan Borgwardt and Thomas Meyer, editors, Proc. 33rd Int. Workshop on Description Logics (DL 2020), volume 2663 of CEUR Workshop Proceedings. CEUR-WS.org, 2020. URL: https://ceur-ws.org/Vol-2663/paper-5.pdf.
  4. Seulkee Baek. A Formally Verified Checker for First-Order Proofs. In Liron Cohen and Cezary Kaliszyk, editors, Proc. 12th Int. Conf. on Interactive Theorem Proving (ITP'21), volume 193 of LIPIcs, pages 6:1-6:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.6.
  5. Henk Barendregt and Freek Wiedijk. The challenge of computer mathematics. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, 363(1835):2351-2375, 2005. URL: https://doi.org/10.1098/rsta.2005.1650.
  6. Véronique Benzaken, Evelyne Contejean, and Ştefania-Gabriela Dumbravă. Certifying standard and stratified datalog inference engines in ssreflect. In Mauricio Ayala-Rincón and César A. Muñoz, editors, Proc. 8th Int. Conf. on Interactive Theorem Proving (ITP'17), volume 10499 of LNCS, pages 171-188. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66107-0_12.
  7. Angela Bonifati, Ştefania-Gabriela Dumbravă, and Emilio Jesús Gallego Arias. Certified graph view maintenance with regular datalog. Theory Pract. Log. Program., 18(3-4):372-389, 2018. URL: https://doi.org/10.1017/S1471068418000224.
  8. Florent Bréhard, Assia Mahboubi, and Damien Pous. A Certificate-Based Approach to Formally Verified Approximations. In John Harrison, John O'Leary, and Andrew Tolmach, editors, Proc. 10th Int. Conf. on Interactive Theorem Proving (ITP'19), volume 141 of LIPIcs, pages 8:1-8:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.8.
  9. Peter Buneman, Sanjeev Khanna, and Wang Chiew Tan. Why and where: A characterization of data provenance. In Jan Van den Bussche and Victor Vianu, editors, Proc. 8th Int. Conf. on Database Theory (ICDT'01), volume 1973 of LNCS, pages 316-330. Springer, 2001. URL: https://doi.org/10.1007/3-540-44503-X_20.
  10. Marco Calautti, Ester Livshits, Andreas Pieris, and Markus Schneider. The complexity of why-provenance for datalog queries. Proc. ACM Manag. Data, 2(2):83, 2024. URL: https://doi.org/10.1145/3651146.
  11. Andrea Calì, Georg Gottlob, and Thomas Lukasiewicz. A general datalog-based framework for tractable query answering over ontologies. In Jan Paredaens and Jianwen Su, editors, Proc. 28th Symposium on Principles of Database Systems (PODS'09), pages 77-86. ACM, 2009. URL: https://doi.org/10.1145/1559795.1559809.
  12. David Carral, Markus Krötzsch, and Jacopo Urbani. Practical uses of existential rules in knowledge representation. Tutorial at the 24th European Conference on Artificial Intelligence (ECAI'20); lecture materials online at https://iccl.inf.tu-dresden.de/web/Rules_ECAI_Tutorial_2020/en, 2020.
  13. Stefano Ceri, Georg Gottlob, and Letizia Tanca. Logic Programming and Databases. Springer, 1990. Google Scholar
  14. Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. Introduction to Algorithms, Third Edition. The MIT Press, 3rd edition, 2009. Google Scholar
  15. Ştefania-Gabriela Dumbravă. Formalisation en Coq de Bases de Données Relationnelles et Déductives -et Mécanisation de Datalog. PhD thesis, Université Paris Saclay (COmUE), 2016. Google Scholar
  16. Ali Elhalawati, Markus Krötzsch, and Stephan Mennicke. An existential rule framework for computing why-provenance on-demand for datalog. In Guido Governatori and Anni-Yasmin Turhan, editors, Proc. 2nd Int. Joint Conf. on Rules and Reasoning (RuleML+RR'22), volume 13752 of LNCS, pages 146-163. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-21541-4_10.
  17. Asta Halkjær From and Frederik Krogsdal Jacobsen. Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL. In June Andronick and Leonardo de Moura, editors, Proc. 13th Int. Conf. on Interactive Theorem Proving (ITP'22), volume 237 of LIPIcs, pages 13:1-13:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.ITP.2022.13.
  18. Martin Gebser, Roland Kaminski, Benjamin Kaufmann, and Torsten Schaub. Multi-shot ASP solving with clingo. Theory Pract. Log. Program., 19(1):27-82, 2019. URL: https://doi.org/10.1017/S1471068418000054.
  19. Todd J. Green, Gregory Karvounarakis, and Val Tannen. Provenance semirings. In Proceedings of the Twenty-Sixth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, June 11-13, 2007, Beijing, China, pages 31-40, 2007. URL: https://doi.org/10.1145/1265530.1265535.
  20. Marijn Heule, Warren Hunt, Matt Kaufmann, and Nathan Wetzler. Efficient, verified checking of propositional proofs. In Mauricio Ayala-Rincón and César A. Muñoz, editors, Proc. 8th Int. Conf. on Interactive Theorem Proving (ITP'17), volume 10499 of LNCS, pages 269-284. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66107-0_18.
  21. Alex Ivliev, Lukas Gerlach, Simon Meusel, Jakob Steinberg, and Markus Krötzsch. Nemo: Your Friendly and Versatile Rule Reasoning Toolkit. In Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning, pages 743-754, August 2024. URL: https://doi.org/10.24963/kr.2024/70.
  22. Herbert Jordan, Bernhard Scholz, and Pavle Subotic. Soufflé: On synthesis of program analyzers. In Swarat Chaudhuri and Azadeh Farzan, editors, Computer Aided Verification - 28th Int. Conf. (CAV'16), volume 9780 of LNCS, pages 422-430. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-41540-6_23.
  23. Yevgeny Kazakov, Markus Krötzsch, and František Simančík. The incredible ELK: From polynomial procedures to efficient reasoning with EL ontologies. J. of Automated Reasoning, 53:1-61, 2013. Google Scholar
  24. Markus Krötzsch. Efficient rule-based inferencing for OWL EL. In Toby Walsh, editor, Proc. 22nd Int. Joint Conf. on Artificial Intelligence (IJCAI'11), pages 2668-2673. AAAI Press/IJCAI, 2011. URL: https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-444.
  25. Muhammad Numair Mansur, Maria Christakis, and Valentin Wüstholz. Metamorphic testing of datalog engines. In Proc. of the 29th ACM Joint Meeting on European Software EngineeringConf. and Symposium on the Foundations of Software Engineering (ESEC/FSE'21), pages 639-650. ACM, 2021. URL: https://doi.org/10.1145/3468264.3468573.
  26. Muhammad Numair Mansur, Valentin Wüstholz, and Maria Christakis. Dependency-aware metamorphic testing of datalog engines. In Proc. 32nd ACM SIGSOFT Int. Symposium on Software Testing and Analysis (ISSTA'23). ACM, 2023. URL: https://doi.org/10.1145/3597926.3598052.
  27. Maximilian Marx and Markus Krötzsch. Tuple-generating dependencies capture complex values. In Dan Olteanu and Nils Vortmeier, editors, Proc. 25th Int. Conf. on Database Theory (ICDT'22), volume 220 of LIPIcs, pages 13:1-13:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.ICDT.2022.13.
  28. Ross M. McConnell, Kurt Mehlhorn, Stefan Näher, and Pascal Schweitzer. Certifying algorithms. Comput. Sci. Rev., 5(2):119-161, 2011. URL: https://doi.org/10.1016/J.COSREV.2010.09.009.
  29. Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction - CADE 28, pages 625-635. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_37.
  30. Yavor Nenov, Robert Piro, Boris Motik, Ian Horrocks, Zhe Wu, and Jay Banerjee. RDFox: A highly-scalable RDF store. In Marcelo Arenas, Óscar Corcho, Elena Simperl, Markus Strohmaier, Mathieu d'Aquin, Kavitha Srinivas, Paul T. Groth, Michel Dumontier, Jeff Heflin, Krishnaprasad Thirunarayan, and Steffen Staab, editors, Proc. 14th Int. Semantic Web Conf. (ISWC'15), Part II, volume 9367 of LNCS, pages 3-20. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-25010-6_1.
  31. Yann Ramusat, Silviu Maniu, and Pierre Senellart. Efficient provenance-aware querying of graph databases with datalog. In Proc. 5th ACM SIGMOD Joint Int. Workshop on Graph Data Management Experiences & Systems and Network Data Analytics (GRADES-NDA'22). ACM, 2022. URL: https://doi.org/10.1145/3534540.3534689.
  32. Anders Schlichtkrull, Rene Rydhof Hansen, and Flemming Nielson. Isabelle-verified correctness of datalog programs for program analysis. In Proc. 39th ACM/SIGAPP Symposium on Applied Computing (SAC 2024), pages 1731-1734. ACM, 2024. URL: https://doi.org/10.1145/3605098.3636091.
  33. Johannes Tantow, Lukas Gerlach, Stephan Mennicke, and Markus Krötzsch. knowsys/CertifyingDatalog. Software, version 0.2.0., (visited on 2025-09-03). URL: https://github.com/knowsys/CertifyingDatalog/tree/v0.2.0
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.23826
  34. Jacopo Urbani, Ceriel Jacobs, and Markus Krötzsch. Column-oriented Datalog materialization for large knowledge graphs. In Dale Schuurmans and Michael P. Wellman, editors, Proc. 30th AAAI Conf. on Artificial Intelligence (AAAI'16), pages 258-264. AAAI Press, 2016. URL: https://doi.org/10.1609/AAAI.V30I1.9993.
  35. Niels van der Weide, Deivid Vale, and Cynthia Kop. Certifying Higher-Order Polynomial Interpretations. In Adam Naumowicz and René Thiemann, editors, Proc. 14th Int. Conf. on Interactive Theorem Proving (ITP'23), volume 268 of LIPIcs, pages 30:1-30:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.ITP.2023.30.
  36. Nathan Whitehead. A certified distributed security logic for authorizing code. In Thorsten Altenkirch and Conor McBride, editors, Types for Proofs and Programs, pages 253-268. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74464-1_17.
  37. Chi Zhang, Linzhang Wang, and Manuel Rigger. Finding Cross-Rule Optimization Bugs in Datalog Engines. Proc. ACM Program. Lang., 8(OOPSLA1):110-136, 2024. URL: https://doi.org/10.1145/3649815.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact