Mace4*

Models And Counter-Examples

This page is obsolete. Mace4 is now being maintained elsewhere.

Abstract

Mace4 is a program that searches for finite models of first-order formulas. For a given domain size, all instances of the formulas over the domain are constructed. The result is a set of ground clauses with equality. Then, a decision procedure based on ground equational rewriting is applied. If satisfiability is detected, one or more models are printed. Mace4 is a useful complement to first-order theorem provers, with the prover searching for proofs and Mace4 looking for countermodels, and it is useful for work on finite algebras. Mace4 performs better on equational problems than our previous model-searching program Mace2.

Fun and Games: Solving Sudoku puzzles with Mace4

The Distribution Package

The current version of Mace4 for unix-like systems (July-2005) is packaged with Prover9. See the Prover9 Quickstart Page for notes on downloading and installing Mace4 and Prover9.

A previous version of Mace4 has been compiled for Microsoft Windows: mace4-2004-C-win.zip (May 2004). This contains a Windows binary only (command line).

Documentation

The Mace4 manual in PDF
The Mace4 manual in PostScript
An important change, starting with the July-2005 version: the negation symbol has been changed from ~ (tilde) to - (hyphen). This change was for compatibility with other deduction systems.

Examples

You can browse the sample problems in the distribution package.
Here is an example of a Perl program that calls Mace4.
Here are examples with the auxiliary programs.

Copyrights and License

See the Otter/MACE Legal Page.

* The spice, not the weapon.

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