Usage and Hints

Automatic mode

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

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.

Even more problems will typically be solved with strategy scheduling. Use

eprover --auto-scheduling=<cores> --cpu-limit=300 problem.p

<cores> is the number of CPU cores to be used. Both cores and CPU limit are used to adapt the schedule, but will assume reasonable defaults if omitted.

Answer substitutions

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.

      fof(socrates,axiom,(philosopher(socrates))).
      fof(plato,axiom,(philosopher(plato))).
      fof(hume,axiom,(philosopher(hume))).
      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 :

eprover --answers=2 ans_test01.p

Documentation

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

• 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.

• E comes with UNIX man pages for the major executables, including eprover, eground, 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

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

• 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.
• Finally, there are a number of technical papers on E. Some of them are listed on the References page, which also contains further links.

Reporting bugs

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:

• The output of eprover --version.
• The full command line you used to start the prover.
• The smallest possible input file demonstrating the bug.