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 isomorphism 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).