Prover 9 and Mace 4
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.
DocumentationManuals are here: http://www.cs.unm.edu/~mccune/prover9/manual-examples.html
released on 4 November 2009
|License||Verified by||Verified on||Notes|
|GPLv2orlater||Deborah Nicholson||24 June 2008|
Leaders and contributors
Resources and communication
This entry (in part or in whole) was last reviewed on 3 March 2017.