GitPedia

Prover9

Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples.

From ai4reason·Updated June 26, 2026·View on GitHub·

This is Prover9, an automated theorem prover and model finder for first-order logic with equality. The project is written primarily in C, distributed under the GNU General Public License v2.0 license, first published in 2018. Key topics include: computer-science, first-order-logic, logic, mathematics, model-checking.

Prover9

This is Prover9, an automated theorem prover and model finder for
first-order logic with equality.

This clone is based on the version LADR-2017-11A provided by Bob Veroff, the
most recent version in August 2018.

Readme first

Prover9, Mace4, and Related Programs.

To compile, see README.make.

See

http://www.cs.unm.edu/~mccune/prover9/

for the HTML manual, examples, and updates.

Contributors

Showing top 1 contributor by commit count.

cbboyan

cbboyan

5 commits

View all contributors on GitHub →

This article is auto-generated from ai4reason/Prover9 via the GitHub API.Last fetched: 6/26/2026