← All papers
Verifying Datalog Reasoning with Lean
cs.LO
Sep 1, 2025 · v1
TL;DR
Builds a certified Datalog reasoning checker in Lean 4 for verifying rule-based inference results.
Abstract
This paper presents a framework for verifying Datalog reasoning results in the Lean 4 theorem prover. The authors develop a certified checker that can verify the output of Datalog engines, ensuring that derived facts are correct consequences of the input rules and facts. The approach bridges the gap between efficient Datalog evaluation and formally verified correctness guarantees.
Problem
Datalog engines compute derived facts efficiently but provide no formal correctness guarantee that the results are valid consequences of the input rules and facts.
Approach
The authors develop a certified checker in Lean 4 that verifies the output of Datalog engines. The checker ensures that derived facts follow correctly from input rules and facts, bridging efficient Datalog evaluation with formally verified correctness guarantees.
Results
A working framework for verifying Datalog reasoning results in Lean 4 is presented, providing certified correctness of Datalog engine outputs.