Refutation Prover for FOL using First-Order Resolution
-
Updated
Nov 12, 2018 - Python
Refutation Prover for FOL using First-Order Resolution
Demonstration of BDD-based SAT solver that generates checkable proofs of unsatisfiability. Details provided in paper: R. E. Bryant and M. J. H. Heule, "Generating Extended Resolution Proofs in a BDD-based SAT Solver," TACAS 2021
Add a description, image, and links to the resolution-proof topic page so that developers can more easily learn about it.
To associate your repository with the resolution-proof topic, visit your repo's landing page and select "manage topics."