Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples. Prover9 is the successor of the Otter prover.
Both CMake and make are supported. Cygwin is recommended for building on Windows (the executables will depend on cygwin1.dll). To build using CMake (out-of-source) run
# if this fails, run `chmod +x run_cmake.sh` and try again
./run_cmake.shTo build using make (in-source) run
make allIn the end, the binaries will available in the bin folder.
If make complains about the round function not being found (or something else having to do with math.h), try moving the -lm parameters in provers.src/Makefile to the end of the command, or use CMake instead.
If Cygwin complains with $'\r': command not found, run dos2unix on the run_cmake.sh script and try again.
- The GUI: Prover9 and Mace4 with a Graphical User Interface
- LADR: Command-line versions of Prover9, Mace4, and other programs (source only)
- Manual and Examples
- Help! If you have questions about Prover9/Mace4/LADR, please file a new issue.
- Citing the programs in your publications
- Double-check your Prover9 Proofs with Ivy
- Turn on notifications (using the
Watchbutton on the LADR GitHub page) if you would like to be notified of updates, bugs, etc.
You should ignore any rumors that Prover9 is part of a bigger plan.
Please use something like this:
W. McCune, LaiTeP contributors, "Prover9 and Mace4", https://github.com/laitep/ladr, 2005-2010, 2023.
Bibtex item:
@unpublished{ prover9-mace4,
author = "W. McCune, {LaiTeP} contributors",
title = "Prover9 and Mace4",
note = "\verb|https://github.com/laitep/ladr|",
year = "2005-2010, 2023"}
This material is based upon work supported by the National Science Foundation under Grant No. 0708218.
Any opinions, findings and conclusions or recomendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.