Man Linux: Main Page and Category List

NAME

       mace4 - searches for finite countermodels of first-order statements

SYNOPSIS

       mace4 [options] < input-file > output-file

DESCRIPTION

       This manual page documents briefly the mace4 command.

       The program mace4 searches for finite structures satisfying first-order
       and equational statements, the same kind of statement  that  prover9(1)
       accepts.  If  the  statement  is  the  denial  of  some conjecture, any
       structures found by mace4 are counterexamples to the conjecture.  mace4
       can be a valuable complement to prover9(1), looking for counterexamples
       before (or at the same time as) using prover9(1) to search for a proof.
       It  can  also  be  used  to  help  debug input clauses and formulas for
       prover9(1).

OPTIONS

       A  summary  of  options  is  included  below.   Options  override   the
       equivalent  settings  given in the input file.  To set or clear a flag,
       you must give 1 or 0 as the value.

       -help  This tells mace4  to  print  a  summary  of  these  command-line
              options.

       -n n   This  gives the starting domain size for the search. The default
              value is 2. If you also give an -N option,  mace4  will  iterate
              domain  sizes  up through the -N value, using an increment given
              by the -I value. Otherwise, mace4 will search only  for  the  -n
              value.

       -N n   This gives the ending domain size for the search. The default is
              10.

       -i n   This gives the domain size increment for the search. The default
              is 1.

       -q n   This  flag  overrides  the parameter iterate. It says to try the
              sizes that are prime numbers, from -n up through -N.

       -m n   Stop searching when the  nth  structure  has  been  found.   The
              default is 1.

       -t n   Stop searching after n seconds.

       -s n   Allow  at most n seconds for each domain size. The parameter can
              be used (together with -t) to give an overall time limit.

       -b n   Stop searching when (about) n  megabytes  of  memory  have  been
              used.

       -V n   A  rule is needed for distinguishing variables from constants in
              clauses and formulas with free variables. If this flag is clear,
              variables  start with (lower case) ‘u’ through ‘z’. If this flag
              is set, variables in clauses start with (upper case) ‘A’ through
              ‘Z’ or ‘_’.

       -P n   If  this  flag is set, all structures that are found are printed
              in ‘standard’ form, which means they are suitable  as  input  to
              other LADR programs such as isofilter(1) and interpformat(1).

       -p n   If this flag is set, and if -P is clear, all structures that are
              found are printed in a tabular form.

       -R n   If this flag is set, a ring  structure  is  is  applied  to  the
              search.  The  operations  {+,-,*}  are assumed to be the ring of
              integers (mod domain_size). This method puts a tight  constraint
              on   the   search,   allowing   much  larger  structures  to  be
              investigated.

       -v n   If this flag is set, the output file receives information  about
              the search, including the initial partial model (the part of the
              model that can be determined  before  backtracking  starts)  and
              timing  and  other statistics for each domain size. (It does not
              give a trace of the backtracking, so it does not consume  a  lot
              of file space.)

       -T n   If the trace flag is set, detailed information about the search,
              including a  trace  of  all  assignments  and  backtracking,  is
              printed  to  the  standard  output.  This  flag  causes a lot of
              output, so it should be used only on small searches.

       There also exist a number of  advanced  options,  which  are  used  for
       experimentation  with search methods. They can be ignored by nearly all
       users. For descriptions  of  these  options,  see  the  original  mace4
       manual.

SEE ALSO

       prover9(1).
       Full  documentation for mace4 is found in the prover9 manual, available
       on    Debian    systems    in    the     prover9-doc     package     at
       /usr/share/doc/prover9-doc/manual/index.html.
       The    original    mace4   manual,   which   can   be   downloaded   at
       http://www.cs.unm.edu/~mccune/prover9/mace4.pdf

AUTHOR

       mace4 was written by William McCune <mccune@cs.unm.edu>

       This manual page was written by Peter Collingbourne  <peter@pcc.me.uk>,
       for the Debian project (but may be used by others).

                                August 12, 2007