eprover
reads a set of first-order clauses and formulae and tries to refute it.
eproof
is a wrapper script that calls
eprover
and then runs
epclextract
on its output to construct a proof.
-h
--help
Print a short description of program usage and options.
-V
--version
Print the version number of the prover. Please include this with all bug
reports (if any).
-v
--verbose[=<arg>]
Verbose comments on the progress of the program. This differs from the
output level (below) in that technical information is printed to stderr,
while the output level determines which logical manipulations of the
clauses are printed to stdout. 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, level 1 will output each clause as it is
processed, level 2 will output generating inferences, level 3 will give a
full protocol including rewrite steps and level 4 will include some
internal clause renamings. Levels >= 2 also imply PCL2 or TSTP formats
(which can be post-processed with suitable tools).
--pcl-terms-compressed
Print terms in the PCL output in shared representation.
--pcl-compact
Print PCL steps without additional spaces for formatting (safes disk
space for large protocols).
--print-statistics
Print the inference statistics (only relevant for output level 0,
otherwise they are printed automatically.
--print-detailed-statistics
Print data about the proof state that is potentially expensive to
collect. Includes number of term cells and number of rewrite steps.
-S
--print-saturated[=<arg>]
Print the (semi-) saturated clause sets after terminating the saturation
process. The argument given describes which parts should be printed in
which order. Legal characters are 'eigEIGaA', standing for processed
positive units, processed negative units, processed non-units,
unprocessed positive units, unprocessed negative units, unprocessed
non-units, and two types of additional equality axioms, respectively.
Equality axioms will only be printed if the original specification
contained real equality. In this case, 'a' requests axioms in which a
separate substitutivity axiom is given for each argument position of a
function or predicate symbol, while 'A' requests a single substitutivity
axiom (covering all positions) for each symbol. The short form or the
long form without the optional argument is equivalent to
--print-saturated=eigEIG.
--print-sat-info
Print additional information (clause number, weight, etc) as a comment
for clauses from the semi-saturated end system.
--filter-saturated[=<arg>]
Filter the (semi-) saturated clause sets after terminating the
saturation process. The argument is a string describing which operations
to take (and in which order). Options are 'u' (remove all clauses with
more than one literal), 'c' (delete all but one copy of identical
clauses, 'n', 'r', 'f' (forward contraction, unit-subsumption only, no
rewriting, rewriting with rules only, full rewriting, respectively), and
'N', 'R' and 'F' (as their lower case counterparts, but with
non-unit-subsumption enabled as well). The option without the optional
argument is equivalent to --filter-saturated=Fc.
--cnf
Convert the input problem into clause normal form and print it. This is
(nearly) equivalent to '--print-saturated=eigEIG
--processed-clauses-limit=0' and will by default perform some usually
useful simplifications. You can additionally specify e.g.
'--no-preprocessing' if you want just the result of CNF translation.
--print-pid
Print the process id of the prover as a comment after option processing.
--error-on-empty
Return with an error code if the input file contains no clauses.
Formally, the empty clause set (as an empty conjunction of clauses) is
trivially satisfiable, and E will treat any empty input set as
satisfiable. However, in composite systems this is more often a sign that
something went wrong. Use this option to catch such bugs.
-m <arg>
--memory-limit=<arg>
Limit the memory the prover may use. The argument is the allowed amount
of memory in MB. If you use the argument 'Auto', the system will try to
figure out the amount of physical memory of your machine and claim most
of it. This option may not work everywhere, due to broken and/or strange
behaviour of setrlimit() in some UNIX implementations, and due to the
fact that I know of no portable way to figure out the physical memory in
a machine. Both the option and the 'Auto' version do work under all
tested versions of Solaris and GNU/Linux. Due to problems with limit
datatypes, it is currently impossible to set a limit of more than 2 GB
(2048 MB).
--cpu-limit[=<arg>]
Limit the cpu time the prover should run. The optional argument is the
CPU time in seconds. The prover 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, MacOS-X, and GNU/Linux. As a side effect, this option will inhibit
core file writing. Please note that if you use both --cpu-limit and
--soft-cpu-limit, the soft limit has to be smaller than the hard limit to
have any effect. The option without the optional argument is equivalent
to --cpu-limit=300.
--soft-cpu-limit[=<arg>]
Limit the cpu time the prover should spend in the main saturation phase.
The prover will then terminate gracefully, i.e. it will perform
post-processing, filtering and printing of unprocessed clauses, if these
options are selected. Note that for some filtering options (in particular
those which perform full subsumption), the postprocessing time may well
be larger than the saturation time. This option is particularly useful if
you want to use E as a preprocessor or lemma generator in a larger
system. The option without the optional argument is equivalent to
--soft-cpu-limit=290.
-R
--resources-info
Give some information about the resources used by the prover. 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.
-C <arg>
--processed-clauses-limit=<arg>
Set the maximal number of clauses to process (i.e. the number of
traversals of the main-loop).
-P <arg>
--processed-set-limit=<arg>
Set the maximal size of the set of processed clauses. This differs from
the previous option in that redundant and back-simplified processed
clauses are not counted.
-U <arg>
--unprocessed-limit=<arg>
Set the maximal size of the set of unprocessed clauses. This is a
termination condition, not something to use to control the deletion of
bad clauses. Compare --delete-bad-limit.
-T <arg>
--total-clause-set-limit=<arg>
Set the maximal size of the set of all clauses. See previous option.
-n
--eqn-no-infix
In LOP, print equations in prefix notation equal(x,y).
-e
--full-equational-rep
In LOP. print all literals as equations, even non-equational ones.
--tptp-in
Parse TPTP-2 format instead of E-LOP (but note that includes are handled
according to TPTP-3 semantics).
--tptp-out
Print TPTP format instead of E-LOP. Implies --eqn-no-infix and will
ignore --full-equational-rep.
--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 in E may not be fully conforming at
all times. E works on all TPTP 3.0.1 input files (including includes).
--tstp-out
Print output clauses in TPTP-3 syntax. In particular, for output levels
>=2, write derivations as TPTP-3 derivations (default is PCL).
--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.
--no-preprocessing
Do not perform preprocessing on the initial clause set. Preprocessing
currently removes tautologies and orders terms, literals and clauses in a
certain ("canonical") way before anything else happens. Unless the next
option is set, it will also unfold equational definitions.
--no-eq-unfolding
During preprocessing, abstain from unfolding (and removing) equational
definitions.
--ac-handling[=<arg>]
Select AC handling mode. Preselected is 'DiscardAll', other options are
'None' to disable AC handling, 'KeepUnits', and 'KeepOrientable'. The
option without the optional argument is equivalent to
--ac-handling=KeepUnits.
--ac-non-aggressive
Do AC resolution on negative literals only on processing (by default, AC
resolution is done after clause creation). Only effective if AC handling
is not disabled.
-W <arg>
--literal-selection-strategy=<arg>
Choose a strategy for selection of negative literals. There are two
special values for this option: NoSelection will select no literal (i.e.
perform normal superposition) and NoGeneration will inhibit all
generating inferences. For a list of the other (hopefully
self-documenting) values run 'eprover -W none'. There are two variants of
each strategy. The one prefixed with 'P' will allow paramodulation into
maximal positive literals in addition to paramodulation into maximal
selected negative literals.
--no-generation
Don't perform any generating inferences (equivalent to
--literal-selection-strategy=NoGeneration).
--select-on-processing-only
Perform literal selection at processing time only (i.e. select only in
the _given clause_), not before clause evaluation. This is relevant
because many clause selection heuristics give special consideration to
maximal or selected literals.
-i
--inherit-paramod-literals
Always select the negative literals a previous inference paramodulated
into (if possible). If no such literal exists, select as dictated by the
selection strategy.
-j
--inherit-goal-pm-literals
In a goal (all negative clause), always select the negative literals a
previous inference paramodulated into (if possible). If no such literal
exists, select as dictated by the selection strategy.
-j
--inherit-conjecture-pm-literals
In a conjecture-derived clause), always select the negative literals a
previous inference paramodulated into (if possible). If no such literal
exists, select as dictated by the selection strategy.
--selection-pos-min=<arg>
Set a lower limit for the number of positive literals a clause must have
to be eligible for literal selection.
--selection-pos-max=<arg>
Set a upper limit for the number of positive literals a clause can have
to be eligible for literal selection.
--selection-neg-min=<arg>
Set a lower limit for the number of negative literals a clause must have
to be eligible for literal selection.
--selection-neg-max=<arg>
Set a upper limit for the number of negative literals a clause can have
to be eligible for literal selection.
--selection-all-min=<arg>
Set a lower limit for the number of literals a clause must have to be
eligible for literal selection.
--selection-all-max=<arg>
Set an upper limit for the number of literals a clause must have to be
eligible for literal selection.
--selection-weight-min=<arg>
Set the minimum weight a clause must have to be eligible for literal
selection.
--prefer-initial-clauses
Always process all initial clauses first.
-x <arg>
--expert-heuristic=<arg>
Select one of the clause selection heuristics. Currently at least
available: Auto, Weight, StandardWeight, RWeight, FIFO, LIFO, Uniq,
UseWatchlist. For a full list check HEURISTICS/che_proofcontrol.c. Auto
is recommended if you only want to find a proof. It is special in that it
will also set some additional options. To have optimal performance, you
also should specify -tAuto to select a good term ordering. LIFO is unfair
and will make the prover incomplete. Uniq is used internally and is not
very useful in most cases. You can define more heuristics using the
option -H (see below).
--filter-limit[=<arg>]
Set the limit on the number of 'storage units' in the proof state, after
which the set of unprocessed clauses will be filtered against the
processed clauses to eliminate redundant clauses. As of E 0.7, a 'storage
unit' is approximately one byte, however, storage is estimated in an
abstract way, independent of hardware or memory allocation library, and
the storage estimate is only an approximation. The option without the
optional argument is equivalent to --filter-limit=1000000.
--filter-copies-limit[=<arg>]
Set the number of storage units in new unprocessed clauses after which
the set of unprocessed clauses will be filtered for equivalent copies of
clauses (see above). As this operation is cheaper, you may want to set
this limit lower than --filter-limit. The option without the optional
argument is equivalent to --filter-copies-limit=800000.
--delete-bad-limit[=<arg>]
Set the number of storage units after which bad clauses are deleted
without further consideration. This causes the prover to be potentially
incomplete, but will allow you to limit the maximum amount of memory used
fairly well. The prover will tell you if a proof attempt failed due to
the incompleteness introduced by this option. It is recommended to set
this limit significantly higher than --filter-limit or
--filter-copies-limit. If you select -xAuto and set a memory limit, the
prover will determine a good value automatically. The option without the
optional argument is equivalent to --delete-bad-limit=1500000.
--assume-completeness
There are various way (e.g. the next few options) to configure the prover
to be strongly incomplete in the general case. E will detect when such an
option is selected and return corresponding exit states (i.e. it will not
claim satisfiability just because it ran out of unprocessed clauses). If
you _know_ that for your class of problems the selected strategy is still
complete, use this option to tell the system that this is the case.
--disable-eq-factoring
Disable equality factoring. This makes the prover incomplete for general
non-Horn problems, but helps for some specialized classes. It is not
necessary to disable equality factoring for Horn problems, as Horn
clauses are not factored anyways.
--disable-paramod-into-neg-units
Disable paramodulation into negative unit clause. This makes the prover
incomplete in the general case, but helps for some specialized classes.
--disable-given-clause-fw-contraction
Disable simplification and subsumption of the newly selected given clause
(clauses are still simplified when they are generated). In general, this
breaks some basic assumptions of the DISCOUNT loop proof search
procedure. However, there are some problem classes in which this
simplifications empirically never occurs. In such cases, we can save
significant overhead. The option _should_ work in all cases, but is not
expected to improve things in most cases.
--simul-paramod
Use simultaneous paramodulation to implement superposition. Default is to
use plain paramodulation. This is an experimental feature.
--oriented-simul-paramod
Use simultaneous paramodulation for oriented from-literals. This is an
experimental feature.
--split-clauses[=<arg>]
Determine which clauses should be subject to splitting. The argument is
the binary 'OR' of values for the desired classes:
1:
Horn clauses
2:
Non-Horn clauses
4:
Negative clauses
8:
Positive clauses
16:
Clauses with both positive and negative literals
Each set bit adds that class to the set of clauses which will be split.
The option without the optional argument is equivalent to
--split-clauses=7.
--split-method=<arg>
Determine how to treat ground literals in splitting. The argument is
either '0' to denote no splitting of ground literals (they are all
assigned to the first split clause produced), '1' to denote that all
ground literals should form a single new clause, or '2', in which case
ground literals are treated as usual and are all split off into
individual clauses.
--split-aggressive
Apply splitting to new clauses (after simplification) and before
evaluation. By default, splitting (if activated) is only performed on
selected clauses.
--split-reuse-defs
If possible, reuse previous definitions for splitting.
--reweight-limit[=<arg>]
Set the number of new unprocessed clauses after which the set of
unprocessed clauses will be reevaluated. The option without the optional
argument is equivalent to --reweight-limit=30000.
-t <arg>
--term-ordering=<arg>
Select an ordering type (currently Auto, LPO, LPO4, KBO or KBO1). -tAuto
is suggested, in particular with -xAuto. KBO and KBO1 are different
implementations of the same ordering, KBO is usually faster and has had
more testing. Similarly, LPO4 is an new, equivalent but superior
implementation of LPO.
-w <arg>
--order-weight-generation=<arg>
Select a method for the generation of weights for use with the term
ordering. Run 'eprover -w none' for a list of options.
--order-weights=<arg>
Describe a (partial) assignments of weights to function symbols for term
orderings (in particular, KBO). You can specify a list of weights of the
form 'f1:w1,f2:w2, ...'. Since a total weight assignment is needed, E
will _first_ apply any weight generation scheme specified (or the default
one), and then modify the weights as specified. Note that E performs only
very basic sanity checks, so you probably can specify weights that break
KBO constraints.
-G <arg>
--order-precedence-generation=<arg>
Select a method for the generation of a precedence for use with the term
ordering. Run 'eprover -G none' for a list of options.
-c <arg>
--order-constant-weight=<arg>
Set a special weight > 0 for constants in the term ordering. By default,
constants are treated like other function symbols.
--precedence[=<arg>]
Describe a (partial) precedence for the term ordering used for the proof
attempt. You can specify a comma-separated list of precedence chains,
where a precedence chain is a list of function symbols (which all have to
appear in the proof problem), connected by >, <, or =. If this option is
used in connection with --order-precedence-generation, the partial
ordering will be completed using the selected method, otherwise the
prover runs with a non-ground-total ordering. The option without the
optional argument is equivalent to --precedence=.
--lpo-recursion-limit[=<arg>]
Set a depth limit for LPO comparisons. Most comparisons do not need more
than 10 or 20 levels of recursion. By default, recursion depth is limited
to 1000 to avoid stack overflow problems. If the limit is reached, the
prover assumes that the terms are uncomparable. Smaller values make the
comparison attempts faster, but less exact. Larger values have the
opposite effect. Values up to 20000 should be save on most operating
systems. If you run into segmentation faults while using LPO or LPO4,
first try to set this limit to a reasonable value. If the problem
persists, send a bug report ;-) The option without the optional argument
is equivalent to --lpo-recursion-limit=100.
--restrict-literal-comparisons
Make all literals uncomparable in the term ordering (i.e. do not use the
term ordering to restrict paramodulation, equality resolution and
factoring to certain literals. This is necessary to make
Set-of-Support-strategies complete for the non-equational case (It still
is incomplete for the equational case, but pretty useless anyways).
--sos-uses-input-types
If input is TPTP format, use TPTP conjectures for initializing the Set of
Support. If not in TPTP format, use E-LOP queries (clauses of the form
?-l(X),...,m(Y)). Normally, all negative clauses are used. Please note
that most E heuristics do not use this information at all, it is
currently only useful for certain parameter settings (including the
SimulateSOS priority function).
--destructive-er
Allow destructive equality resolution inferences on pure-variable
literals of the form X!=Y, i.e. replace the original clause with the
result of an equality resolution inference on this literal.
--strong-destructive-er
Allow destructive equality resolution inferences on literals of the form
X!=t (where X does not occur in t), i.e. replace the original clause with
the result of an equality resolution inference on this literal. Unless I
am brain-dead, this maintains completeness, although the proof is rather
tricky.
--destructive-er-aggressive
Apply destructive equality resolution to all newly generated clauses, not
just to selected clauses. Implies --destructive-er.
--forward-context-sr
Apply contextual simplify-reflect with processed clauses to the given
clause.
--forward-context-sr-aggressive
Apply contextual simplify-reflect with processed clauses to new clauses.
Implies --forward-context-sr.
--backward-context-sr
Apply contextual simplify-reflect with the given clause to processed
clauses.
-g
--prefer-general-demodulators
Prefer general demodulators. By default, E prefers specialized
demodulators. This affects in which order the rewrite index is
traversed.
-F <arg>
--forward_demod_level=<arg>
Set the desired level for rewriting of unprocessed clauses. A value of 0
means no rewriting, 1 indicates to use rules (orientable equations) only,
2 indicates full rewriting with rules and instances of unorientable
equations. Default behavior is 2.
--strong-rw-inst
Instantiate unbound variables in matching potential demodulators with a
small constant terms.
-u
--strong-forward-subsumption
Try multiple positions and unit-equations to try to equationally subsume
a single new clause. Default is to search for a single position.
--watchlist[=<arg>]
Give the name for a file containing clauses to be watched for during the
saturation process. If a clause is generated that subsumes a watchlist
clause, the subsumed clause is removed from the watchlist. The prover
will terminate when the watchlist is empty. If you want to use the
watchlist for guiding the proof, put the empty clause onto the list and
use the built-in clause selection heuristic 'UseWatchlist' (or build a
heuristic yourself using the priority functions 'PreferWatchlist' and
'DeferWatchlist'). Use the argument 'Use inline watchlist type' (or no
argument) and the special clause type 'watchlist' if you want to put
watchlist clauses into the normal input stream. This is only supported
for TPTP input formats. The option without the optional argument is
equivalent to --watchlist='Use inline watchlist type'.
--no-watchlist-simplification
Normally, that watchlist is brought into normal form with respect to the
current processed clause set and certain simplifications. This option
disables this behaviour.
--conventional-subsumption
Equivalent to --subsumption-indexing=None.
--subsumption-indexing=<arg>
Determine choice of indexing for (most) subsumption operations. Choices
are 'None' for naive subsumption, 'Direct' for direct mapped FV-Indexing,
'Perm' for permuted FV-Indexing and 'PermOpt' for permuted FV-Indexing
with deletion of (suspected) non-informative features. Default behaviour
is 'Perm'.
--fvindex-featuretypes=<arg>
Select the feature types used for indexing. Choices are "None" to disable
FV-indexing, "AC" for AC compatible features (the default) (literal
number and symbol counts), "SS" for set subsumption compatible features
(symbol depth), and "All" for all features.Unless you want to measure the
effects of the different features, I suggest you stick with the default.
--fvindex-maxfeatures[=<arg>]
Set the maximum initial number of symbols for feature computation.
Depending on the feature selection, a value of X here will convert into
2X+2 features (for set subsumption features), 2X+4 features (for
AC-compatible features) or 4X+6 features (if all features are used, the
default). Note that the actually used set of features may be smaller than
this if the signature does not contain enough symbols.For the Perm and
PermOpt version, this is _also_ used to set the maximum depth of the
feature vector index. Yes, I should probably make this into two separate
options. If you select a small value here, you should probably not use
"Direct" for the --subsumption-indexing option. The option without the
optional argument is equivalent to --fvindex-maxfeatures=200.
--fvindex-slack[=<arg>]
Set the number of slots reserved in the index for function symbols that
may be introduced into the signature later, e.g. by splitting. If no new
symbols are introduced, this just wastes time and memory. If PermOpt is
chosen, the slackness slots will be deleted from the index anyways, but
will still waste (a little) time in computing feature vectors. The option
without the optional argument is equivalent to --fvindex-slack=0.
--simplify-with-unprocessed-units[=<arg>]
Determine whether to use unprocessed unit clauses for simplify-reflect
(unit-cutting) and unit subsumption. Possible values are 'NoSimplify' for
strict DISCOUNT loop, 'TopSimplify' to use unprocessed units at the top
level only, or 'FullSimplify' to use positive units even within
equations. The option without the optional argument is equivalent to
--simplify-with-unprocessed-units=TopSimplify.
-D <arg>
--define-weight-function=<arg>
Define a weight function (see manual for details). Later definitions
override previous definitions.
-H <arg>
--define-heuristic=<arg>
Define a clause selection heuristic (see manual for details). Later
definitions override previous definitions.
--free-numbers
Treat numbers (strings of decimal digits) as normal free function symbols
in the input. By default, number now are supposed to denote domain
constants and to be implicitly different from each other.
--free-objects
Treat object identifiers (strings in double quotes) as normal free
function symbols in the input. By default, object identifiers now
represent domain objects and are implicitly different from each other
(and from numbers, unless those are declared to be free).
--definitional-cnf[=<arg>]
Use the new clausification algorithm that possibly introduces definitions
for subformulas to avoid exponential blow-up. This is now the default.
The optional argument is a fudge factor that determines when a definition
is introduced. 0 disables definitions, the default works well. The option
without the optional argument is equivalent to --definitional-cnf=24.
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
eground(1),
epclextract(1),
PDF manual
/usr/share/doc/eprover/eprover.pdf.gz
for a more detailed description.