Mace4

Mace4 is a finite model finder for first-order logic with equality. It searches for finite interpretations of function and predicate symbols that satisfy a given set of first-order formulas. Developed as part of the Prover9/Mace4 toolkit, it is commonly used to obtain concrete models, counterexamples, or to test satisfiability of logical conjectures.

The program accepts formulas written in a syntax compatible with the Prover9 family and allows the user to request models over a finite domain. By specifying a maximum domain size, Mace4 attempts to construct a structure with that many elements in which all input formulas hold. If such a model exists, Mace4 prints the interpretations of symbols—constants, functions, and predicates—over the finite domain. If no finite model exists for the given size, it reports failure, prompting the user to increase the domain bound or reformulate the problem.

Mace4 is frequently used in automated reasoning, logic education, and formal-methods research. It complements theorem-proving tools by providing concrete models that demonstrate satisfiability or give countermodels to conjectures. The output is designed to be human-readable, enabling investigators to inspect how symbols are interpreted in the constructed model.

Historically, Mace4 follows the earlier Mace model finder and is distributed as part of the Prover9/Mace4 suite, a widely cited package in the automated reasoning community. It remains a practical option for exploring finite semantics of first-order theories, especially when a constructive witness is desired or when educational demonstrations require explicit models. Limitations include potential performance issues on large or highly connected signatures, and the fact that only finite models are accessible.