Prover9 Manual
|
| Version 2008-06A
|
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
with a fatal error.
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(hints). These are intended to help
Prover9 find proofs and are ignored by Mace4.
- formulas(goals). These are negated by Mace4, just as
they are by Prover9.
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" is not particularly intuitive
for Mace4 users, because Mace4 does not prove things.
It makes more sense, however, when one thinks 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.
Next Section:
Mace4 Options