Show HN: An Automated Theorem Proving library inspired by a book by Harrison
github.comI've been working on translating (and modifying) parts of John Harrison's automated theorem proving book from Ocaml into a Rust library.
Highlights so far are an implementation of DPLL with conflict-clause learning that lets us solve hard sudoku problems in less than a second (not competitive w/ SAT solvers like MiniSat, but not bad either), and a Herbrand style semi-decision procedure for first-order validity.
There's lots of room for more sophisticated methods and optimization. More to come soon.
No comments yet.