Mace4 (Models And CounterExamples)

The program Mace4 [McCune-Mace4] searches for finite structures satisfying first-order and equational statements (the same kind of statement that Prover9 accepts). If the statement is the denial of some conjecture, any structures found by Mace4 are counterexamples to the conjecture.

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.

What Mace4 Does

Mace4 searches for unsorted finite structures only. That is, a structure (model) has one underlying finite set, called the domain (the members are always 0,1,...,n-1 for a set of size n), and structures are functions and relations (tables) over the domain, corresponding to the operations and relation symbols in the specification.

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

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.

Next Section: Mace4 Input