MACE*
Models And Counter-Examples
This page is obsolete. Mace2 and Mace4 are
now being maintained
elsewhere.
There are two Mace programs. They are not just different versions of
the same program. The model-searching methods are fundamentally
different. Neither is uniformly better.
Someday we hope to combine them into a single program.
- Mace2
- tends to work better for relational problems,
that is, without deeply nested terms,
- takes the same input files (for the most part) as Otter,
- Mace4
- tends to work better for equational problems, problems with deeply
nested terms, and problems with many variables, and
- takes the same input files as the future generations of
Argonne theorem provers.
* The spice, not the weapon.
These activities are projects of the
Mathematics and Computer Science Division
of
Argonne National Laboratory.