xenial (1) mace4.1.gz

Provided by: prover9_0.0.200911a-2.1_amd64 bug

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                                        MACE4(1)