Usage and Hints

 

If you need any information about using E, first try the documentation that is included with the distribution.


  1. The README file in the top level directory contains basic installation and usage information. You really should re-read it every time you install a new release of E.

  2. E comes with UNIX man pages for the major executables, including eprover, eground, epclextract, and e_axfilter. If you perform a full install e.g. into /usr/local, man should be able to find them. If not, you can directly display the man pages via e.g.

        man E/DOC/man/eprover.1

  1. The programs all support the --help option, which will generate output that is roughly equivalent to the man page.

  2. The E manual is the most detailed, if not always most up-to-date, source of information. You will find it in E/DOC/eprover.pdf.

  3. Finally, there are a number of technical papers on E. Some of them are listed on the References page, which also contains further links.

E comes with a multitude of options, many of which affect proof search and interact in often unexpected ways. The easiest way to get good performance out of the prover is to rely on the automatic mode. For a problem specified in the current TPTP-3/TSTP syntax, the suggested command line (as of E 1.9) is


  1. eprover --auto problem.p


If you have more time than memory, you can also add --memory-limit=Auto or (e.g.) --memory-limit=1024. Note that E will typically perform much better in automatic mode than in the default mode.


For versions of E older than 1.6, use eprover -xAuto -tAuto --tptp3-format problem.p.

Automatic mode

Starting with version 1.3, E is able to provide answer substitutions. It currently adheres to the Tuple version of the TPTP proposal for answer extraction. To use this feature, you need to specify an existentially quantified conjecture formula with the formula type question, as in the example below. This implies the use of the TPTP-3/TSTP syntax.


  1. fof(socrates,axiom,(philosopher(socrates))).

  2. fof(plato,axiom,(philosopher(plato))).

  3. fof(hume,axiom,(philosopher(hume))).

  4. fof(philosphers_exist,question,( ? [X] : (philosopher(X)))).


By default, E will stop searching after the first answer. The --answers option can be used to specify for how many answers E will keep searching :


  1. eprover --auto --answers=2 ans_test01.p

Answer substitutions

If you experience unexpected behavior with E, please try if it persists in the latest released version. If you want to report a bug, please include the following information:


  1. The output of eprover --version.

  2. The full command line you used to start the prover.

  3. The smallest possible input file demonstrating the bug.

Reporting bugs

Documentation