Prover9 Manual Version 2009-02A

Mace4 Input

Mace4 has been designed so that it accepts most Prover9 input files. This allows users to prepare one input file which can be used by Prover9 (to search for proofs) and by Mace4 (to search for counterexamples).

Mace4 Options

Mace4 and Prover9 accept different sets of flags and parameters. In order to use the same input files for both programs, we let Mace4 take its options from the command line instead of from the input file. If Mace4 is given a Prover9 input file, along with the command-line option -c, it will ignore any unrecognized (e.g., Prover9) options in the input file. The Mace4 options are described on the next page.

Formulas (including Clauses)

Mace4 accepts the same formulas and clauses as Prover9. See the page Prover9 Clauses and Formulas.

A Caveat: Domain Elements

In one important case, formulas have different meanings in Prover9 and Mace4:
If a formula contains constants that are natural-numbers, {0,1,...}, Mace4 assumes they are members of the domain of some structure, that is, they are distinct objects; in effect, Mace4 operates under the assumptions 0 ≠ 1, 0 ≠ 2, ... .

To Prover9, natural numbers are just ordinary constants. For example, to Prover9 the statement 0=1 is satisfiable, and to Mace4 it is unsatisfiable.

Because Mace4 assumes that natural-number constants are members of the domain, if a formula contains a natural number that is out of range (≥ n), when searching for a structure of size n), Mace4 will terminate its search for size n (and continue with larger sizes if the specification says to do so).

An Exception. When the flag arithmetic is set, natural numbers outside of {0,1,...,n-1} can occur.

Lists of Formulas (including Clauses)

Prover9 accepts a fixed set of lists of formulas (e.g., assumptions, usable, goals, hints).

Mace4 accepts any lists of formulas. All are treated as ordinary formulas except the following two lists.

formulas(goals)

Prover9 has several restrictions on the goals it accepts (see Prover9 Goals and Denials), and Mace4 has the same restrictions. Mace4 negates goals and translates them to clauses in the same way as Prover9. (The term "goal" might seem to be bad teminology for Mace4 users, because Mace4 does not prove theorems; however, one can think of Mace4 as searching for a counterexample to the goal.)

When there are multiple goals, Mace handles them the same as Prover9. For example, consider the following goals. 

formulas(goals).
  x * y = y * x              # label(commutativity).
  (x * y) * z = x * (y * z)  # label(associativity).
end_of_list.
Logically, this is a disjunction: Prover9 gives a proof if either goal is proved, and Mace4 gives a counterexample if both are falsified. In particular, this pair of goals is equivalent (for both Prover9 and Mace4) to the following pair of assumptions. 
formulas(assumptions).
  exists x exists y (x * y != y * x).
  exists x exists y exists z (x * y) * z != x * (y * z).
end_of_list.

Distinct Objects

Mace4 accepts a shorthand method for stating that sets of objects are distinct. Here is an example of two sets of distinct objects. 
list(distinct).
[a,b,c].     % equivalent to (a!=b & a!=c & b!=c).
[d,e,f(a)].  % equivalent to (d!=e & d!=f(a) & e!=f(a)).
end_of_list.
Although list(distinct) will probably be used mostly for constants and other ground terms, terms with variables can occur.
Next Section: Mace4 Options