# 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

## Examples

##
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.
*