MACE2(1)
NAME
mace2 - searches for finite countermodels of first-order statements
SYNOPSIS
mace2 [options] < input-file > output-file
DESCRIPTION
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.
OPTIONS
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 other constraints.
- -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
- 1.
- -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 only.
- -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 isomor
- phism in quasigroup problems. It applies only to binary function f.
- -h This tells mace2 to print a summary of these command-line
- options.
SEE ALSO
anldp(1), formed(1), otter(1), pl(1). Full documentation for mace2 is found in /usr/share/doc/mace2/mace2.{html,ps.gz}.
AUTHOR
mace2 ws written by William McCune <otter@mcs.anl.gov>
- This manual page was written by Peter Collingbourne
<pcc03@doc.ic.ac.uk>, for the Debian project (but may be used by others).