This repo contains a checker for Datalog proof trees and proofs encoded as directed acyclic graphs.
The checker is implemented and formally verified in Lean 4.
For more details on the usage, take a look into the (subdirectories of the) Examples directory.
Using elan / lake:
lake build
This will download mathlib4 and build the project.
To prevent building mathlib yourself, you can run the following to fetch precompiled dependencies.
lake exe cache get
(You still need to run lake build afterwards.)
The resulting executable is found here: .lake/build/bin/certifyingDatalog
This project is licensed under either of
- Apache License, Version 2.0, (LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0)
- MIT license (LICENSE-MIT or https://opensource.org/licenses/MIT)
at your option.