mace2 - searches for finite countermodels of first-order statements
mace2 [options] < input-file > output-file
This manual page documents briefly the mace2 command.
mace2 is a program that searches for finite models of first-order
statements. The statement to be modeled is first translated to clauses,
then to relational clauses; finally for the given domain size, the
ground instances are constructed. A Davis-Putnam-Loveland-Logeman
procedure decides the propositional problem, and any models found are
translated to first-order models. mace2 is a useful complement to the
theorem prover otter(1), with otter searching for proofs and mace2
looking for countermodels.
A summary of options is included below.
-n n This gives the starting domain size for the search. The default
value is 2. If you also give an -N option, MACE will iterate
domain sizes up through the -N value. Otherwise, mace2 will
search only for the -n value.
-N n This gives the ending domain size for the search. The default is
the value of the -n option.
-c This says that constants in the input should be assigned unique
elements of the domain. If the number of constants in the input
is greater than the domain size n, the first n constants are
given values, and the rest are unconstrained. This is a useful
option because it eliminates lots of isomorphism from the
search. But it can block all models, especially when used with
-p This option tells mace2 to print models in a nice tabular form
as they are found. This format is meant for human consumption.
-P This option tells mace2 to print models in an easily parsable
form. This format has an otter-like syntax and can be read by
most Prolog systems.
-I This option tells mace2 to print models in IVY form. This format
is a Lisp S-expression and is meant to be read by IVY, our proof
and model checker.
-m n This tells mace2 to stop after finding n models. The default is
-t n This tells mace2 to stop after about n seconds. The default is
unlimited. mace2 ignores any assign(max_seconds, n) commands
that might be in the input file. Such commands are used by otter
-k n This tells mace2 to stop if it tries to allocate more than n
kilobytes of memory. The default is 48000 (about 48 megabytes).
mace2 ignores any assign(max_mem, n) commands that might be in
the input file. Such commands are used by otter only.
-x This is a special-purpose constraint designed to reduce
isomorphism in quasigroup problems. It applies only to binary
-h This tells mace2 to print a summary of these command-line
anldp(1), formed(1), otter(1), pl(1).
Full documentation for mace2 is found in
mace2 ws written by William McCune <email@example.com>
This manual page was written by Peter Collingbourne
<firstname.lastname@example.org>, for the Debian project (but may be used by
November 5, 2006