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.
* The spice, not the weapon.

These activities are projects of the Mathematics and Computer Science Division of Argonne National Laboratory.