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

                                        November  5, 2006                                MACE2(1)