NAME
E - The Equational Theorem Prover User Manual
SYNOPSIS
eprover [options] [files]
eproof [options] [files]
DESCRIPTION
E 1.0-004 "Temi"
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.
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
eground(1), epclextract(1),
PDF manual /usr/share/doc/eprover/eprover.pdf.gz for a more detailed
description.