/Prover9

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

Primary LanguageCGNU General Public License v2.0GPL-2.0

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.