Prover9 Manual | Version 2009-11A |
Mace4 can be a valuable complement to Prover9, looking for counterexamples before (or at the same time as) using Prover9 to search for a proof. It can also be used to help debug input clauses and formulas for Prover9.
For the most part, Mace4 accepts the same input files as Prover9. If the input file contains commands that Mace4 does not understand, then the argument "-c" must be given to tell Mace4 to ignore those commands.
For example, say we're learning group theory, and we're wondering whether all groups are commutative. We can run the following two jobs in parallel, with Prover9 looking for a proof, and Mace4 looking for a counterexample.
prover9 -f x2.in > x2.prover9.out mace4 -c -f x2.in > x2.mace4.out
Most of the options accepted by Mace4 can be given either on the command line or in the input file. The following command lists the command-line options accepted by Mace4.
mace4 -help
Terminology. We use the terms interpretation, model, and structure for the objects that Mace4 produces. From a logic point of view, Mace4 produces interpretations which are models of the input formulas. From a math point of view, Mace4 produces structures satisfying the input formulas.
By default, Mace4 starts searching for a structure of domain size 2, and then it increments the size until it succeeds or reaches some limit.
The original Mace4 manual [McCune-Mace4] (PDF) is out of date with respect to features and options, but it contains useful information on the history of Mace4, details on the search methods, and the differences between Mace2 and Mace4.