2 Getting Started

Installation of E should be straightforward. The file README in the main directory of the distribution contains the necessary information. After building, you will find the stand-alone executable E/PROVER/eprover.

E is controlled by a very wide range of parameters. However, if you do not want to bother with the details, you can leave configuration for a problem to the prover. To use this feature, use the following command line options:

-xAuto

Select a literal selection strategy and a selection heuristic automagically (based on problem features).

-tAuto

Select a term ordering automagically.

--memory-limit=xx

Tell the prover how much memory (measured in MB) to use at most. In automatic mode E will optimize its behaviour for this amount (20 MB will work, 64 MB is reasonable, 192 MB is what I use. More is better1, but if you go over your physical memory, you will probably experience very heavy swapping.).

Example: If you happen to have a workstation with 64 MB RAM2, the following command is reasonable:
eprover -xAuto -tAuto --memory-limit=48 PUZ031-1+rm_eq_rstfp.lop

This documentation will probably lag behind the development of the latest version of the prover for quite some time. To find out more about the options available, type eprover --help (or consult the source code included with the distribution).

1Emphasis added for E 0.7 and up, which globally cache rewrite steps.

2Yes, this is outdated. If it still applies to you, get a new computer! It will still work ok, though.