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.

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: