Ubuntu Manpage: eground - manual page for eground 3.2.5

NAME

       eground - manual page for eground 3.2.5

SYNOPSIS

       eground [options] [files]

DESCRIPTION

eground 3.2.5

Read a set of clauses and determine if it can be grounded (i.e. is either already ground
or has no non-constant function symbols). If this is the case, print sufficiently many
ground instances of the clauses to guarantee that a ground refutation can be found for
unsatisfiable clause sets.

Options

-h

--help

Print a short description of program usage and options.

--version

Print the version number of the program.

-v

--verbose[=<arg>]

Verbose comments on the progress of the program by printing technical information
to stderr. The short form or the long form without the optional argument is
equivalent to --verbose=1.

-o <arg>

--output-file=<arg>

Redirect output into the named file.

-s

--silent

Equivalent to --output-level=0.

-l <arg>

--output-level=<arg>

Select an output level, greater values imply more verbose output. Level 0 produces
nearly no output except for the final clauses, level 1 produces minimal additional
output. Higher levels are without meaning in eground (I think).

--print-statistics

Print a short statistical summary of clauses read and generated.

-R

--resources-info

Give some information about the resources used by the system. You will usually get
CPU time information. On systems returning more information with the rusage()
system call, you will also get information about memory consumption.

--suppress-result

Suppress actual printing of the result, just give a short message about success.
Useful mainly for test runs.

--lop-in

Set E-LOP as the input format. If no input format is selected by this or one of the
following options, E will guess the input format based on the first token. It will
almost always correctly recognize TPTP-3, but it may misidentify E-LOP files that
use TPTP meta-identifiers as logical symbols.

--tptp-in

Parse TPTP-2 format instead of E-LOP (except includes, which are handles as in
TPTP-3, as TPTP-2 include syntax is considered harmful).

--tptp-out

Print TPTP-2 format instead of E-LOP.

--tptp-format

Equivalent to --tptp-in and --tptp-out.

--tptp2-in

Synonymous with --tptp-in.

--tptp2-out

Synonymous with --tptp-out.

--tptp2-format

Synonymous with --tptp-format.

--tstp-in

Parse TPTP-3 format instead of E-LOP (Note that TPTP-3 syntax is still under
development, and the version implemented may not be fully conformant at all times.
It works on all TPTP 3.0.1 input files (including includes).

--tstp-out

Print output clauses in TPTP-3 syntax.

--tstp-format

Equivalent to --tstp-in and --tstp-out.

--tptp3-in

Synonymous with --tstp-in.

--tptp3-out

Synonymous with --tstp-out.

--tptp3-format

Synonymous with --tstp-format.

-d

--dimacs

Print output in the DIMACS format suitable for many propositional provers.

--definitional-cnf[=<arg>]

Tune the clausification algorithm to introduces definitions for subformulae to
avoid exponential blow-up. The optional argument is a fudge factor that determines
when definitions are introduced. 0 disables definitions completely. The default
works well. The option without the optional argument is equivalent to
--definitional-cnf=24.

--miniscope-limit[=<arg>]

Set the limit of variables to miniscope per input formula. The build-in default is
1000. Only applies to the new (default) clausification algorithm The option without
the optional argument is equivalent to --miniscope-limit=2147483648.

--split-tries[=<arg>]

Determine the number of tries for splitting. If 0, no splitting is performed. If 1,
only variable-disjoint splits are done. Otherwise, up to the desired number of
variable permutations is tried to find a splitting subset. The option without the
optional argument is equivalent to --split-tries=1.

-U

--no-unit-subsumption

Do not check if clauses are subsumed by previously encountered unit clauses.

-r

--no-unit-resolution

Do not perform forward-unit-resolution on new clauses.

-t

--no-tautology-detection

Do not perform tautology deletion on new clauses.

-m <arg>

--memory-limit=<arg>

Limit the memory the system may use. The argument is the allowed amount of memory
in MB. This option may not work everywhere, due to broken and/or strange behaviour
of setrlimit() in some UNIX implementations. It does work under all tested versions
of Solaris and GNU/Linux.

--cpu-limit[=<arg>]

Limit the cpu time the program should run. The optional argument is the CPU time in
seconds. The program will terminate immediately after reaching the time limit,
regardless of internal state. This option may not work everywhere, due to broken
and/or strange behaviour of setrlimit() in some UNIX implementations. It does work
under all tested versions of Solaris, HP-UX and GNU/Linux. As a side effect, this
option will inhibit core file writing. The option without the optional argument is
equivalent to --cpu-limit=300.

--soft-cpu-limit[=<arg>]

Limit the cpu time spend in grounding. After the time expires, the prover will
print an partial system. The option without the optional argument is equivalent to
--soft-cpu-limit=310.

-i

--add-one-instance

If the grounding procedure runs out of time or memory, try to add at least one
instance of each clause to the set. This might fail for really large clause sets,
since the reserve memory kept for this purpose may be insufficient.

-g <arg>

--give-up=<arg>

Give up early if the problem is unlikely to be reasonably small. If run without
constraints, the program will give up if the clause with the largest number of
instances will be expanded into more than this number of instances. If run with
constraints, the program keeps a running count and will terminate if the estimated
total number of clauses would exceed this value . A value of 0 will leave this test
disabled.

-c

--constraints

Use global purity constraints to restrict the number of instantiations done.

-C

--local-constraints

Use local purity constraints to further restrict the number of instantiations done.
Implies the previous option. Not yet implemented! Note to self: Split clauses need
to get fresh variables if this is to work!

-M

--fix-minisat

Fix the preamble to include only the maximum variable index, to compensate for
MiniSAT's problematic interpretation of the DIMAC syntax.

REPORTING BUGS

       Report bugs to <schulz@eprover.org>. Please include the following, if possible:

       * The version of the package as reported by eprover --version.

       * The operating system and version.

       * The exact command line that leads to the unexpected behaviour.

       * A description of what you expected and what actually happened.

       * If possible all input files necessary to reproduce the bug.

COPYRIGHT

This program is a part of the distribution of the equational theorem prover E. You can
find the latest version of the E distribution as well as additional information at
http://www.eprover.org

This program is free software; you can redistribute it and/or modify it under the terms of
the GNU General Public License as published by the Free Software Foundation; either
version 2 of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY;
without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
See the GNU General Public License for more details.

You should have received a copy of the GNU General Public License along with this program
(it should be contained in the top level directory of the distribution in the file
COPYING); if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330,
Boston, MA 02111-1307 USA

We welcome bug reports and even reasonable questions. If the prover behaves in an
unexpected way, please include the following information:

- What did you observe? - What did you expect? - The output of `eprover --version` - The
full commandline that lead to the unexpected behaviour - The input file(s) that lead to
the unexpected behaviour

Most bug reports should be send to <schulz@eprover.org>. Bug reports with respect to the
HO-version should be send to or at least copied to <jasmin.blanchette@gmail.com>. Please
remember that this is an unpaid volunteer service.

The original copyright holder can be contacted via email or as

Stephan Schulz DHBW Stuttgart Fakultaet Technik Informatik Lerchenstrasse 1 70174
Stuttgart Germany