NAME
E - The Equational Theorem Prover User Manual
SYNOPSIS
eground [options] [files]
DESCRIPTION
eground 0.4
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.
-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
Supress actual printing of the result, just give a short message
about success. Useful mainly for test runs.
--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.
--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 programm 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 contraints,
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!
AUTHOR
Stephan Schulz <schulz@eprover.org>
COPYRIGHT
Copyright 1998-2006 by Stephan Schulz <schulz@eprover.org>
You can find the latest version of E and 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
The original copyright holder can be contacted as
Stephan Schulz (I4)
Technische Universitaet Muenchen
Institut fuer Informatik
Boltzmannstrasse 3
85748 Garching bei Muenchen
Germany
SEE ALSO
epclextract(1). eprover(1),