Man Linux: Main Page and Category List

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