Repository files navigation

This assumes that you have GNU tar, sh and gawk in your search path!

Simple installation of the first-order version (will installexecutables):

  tar -xzf E.tgzcd E  ./configure --bindir=/path/to/EXECDIR  make  make install  /path/to/EXECDIR/eprover -h| more

Simplest installation (in-place):

  tar -xzf E.tgzcd E  ./configure  make rebuildcd PROVER  ./eprover -h| more

Read the rest of this file and the fine (if incomplete) manual ifanything fails. There should be a copy of the manual inDOC/eprover.pdf.

E 3.2 supports (monomorphic) higher-order logic. To build a binarythat supports higher-order reasoning, use the following:

  ./configure --enable-ho  make rebuildcd PROVER  eprover-ho -h| more

The recommended command for running E on the file problem.p is

  eprover --auto --proof-object problem.p

If you want to try the usually stronger strategy scheduling mode(particularly recommended for higher-order problems, use

  eprover --auto-schedule --proof-object problem.p

To use more than one CPU, use something like

  eprover --auto-schedule=8 --proof-object problem.p

Replaceeprover byeprover-ho for the higher-order-enabledversion.You can add a time limit of 300 seconds with the option--cpu-limit=300 and a memory limit of 2 GB with--memory-limit=2048for all "automatic" modes. You can reduce output with-s (or--silent). As of version 1.9.1, E will try to auto-detect the inputformat and adjust the output format accordingly. You can still forceinput and output formats via commandline options.

This is the README file for version 3.2 "Puttabong Moondrop" of the Eequational theorem prover. This version of E is free software, see thefile COPYING for details about the license and the fact that THERE ISNO WARRANTY!

E is an equational theorem prover. That means it is a program that youcan stuff a mathematical specification (in many-sorted first-orderlogic with equality or in polymorphic higher-order logic) and ahypothesisconjecture into, and which will then run forever, using upall of your machines resources. Very occasionally it will find a prooffor the conjecture and tell you so ;-).

E has been created and is currently maintained by Stephan Schulz,schulz@eprover.org, now with the help of several contributors (seeDOC/CONTRIBUTORS). It is developed and distributed under the GNUGeneral Public License.

The E homepage can be found athttps://www.eprover.org

E can be installed anywhere in the file system, either by a normaluser or by the system administrator. By default, the prover will stillbe compiled as a version that supports first-order logic only.

To install the package, unpack the distribution (if you are readingthis, you probably already did):

   gunzip -c E.tgz|tar -xvf -

or

   (g)tar -xzf E.tgz

(if you have GNU tar)

This should create a directory named E. After unpacking, optionallyeditE/Makefile.vars to your liking. In particular, if building forHPUX, comment out the suitable CFLAGS definition (for most systems,the default definition should be ok). Then change to the E directory:

cd E

Determine if you want to run E from its own build directory or wetheryou want to install the executables in some other directoryEXECDIR. In the first case, run

   ./configure

otherwise

   ./configure --bindir=EXECDIR

or, if you also want to install the man-pages into MANDIR,

   ./configure --bindir=EXECDIR --man-prefix=MANDIR

To enable higher-order-support, add the option--enable-ho, e.g.

   ./configure --enable-ho

Then type

   make

to compile the libraries and all included programs under the Edirectory. If you want to install E in a particular EXECDIR, type

   make install

You must have write permission in the EXECDIR, so if you install Eoutside your own home directory, you may need to become root or usesudo.

If you have changed the configuration, you need to rebuild all objectand binary files. Run

   make rebuild

instead of plain make.

Type

   make documentation

to translate the LaTeX documentation (this requires LaTeX2e, pdflatex,and the packages theorem, amssymb and epsfig, which are included inmost current LaTeX distributions). The manual should also be includedas a pre-compiled PDF.

For some operating systems, especially if you do not have the GNU gcccompiler installed, you may need to edit Makefile.vars manually toselect tools and options. If you have any problems, look intoE/DOC/PORTING.

If you get into trouble,

   make rebuild

will rebuild E completely to your current configuration.

After installation, go to E/PROVER and type

   ./eprover BOO001-1+rm_eq_rstfp.lop

to see the prover in action. Type

   ./eprover LUSK6.lop

for a harder example../eprover -h will give you some information anda list of options.

For impatient people who do not want to read anything:

   eprover --auto --memory-limit=<80%_of_your_main_memory><problem-file>

should give a reasonable performance on a large class of problems(unless your main memory is really small).

The auto mode will perform a heuristic pruning of the axiom set whichmay result in incompleteness for very large problems (many thousandsof axioms). If you need completeness, use

  eprover --satauto --memory-limit=<80%_of_your_main_memory><problem-file>

In general, different proof problems are easy for differentstrategies. If you run

  eprover --auto-schedule --memory-limit=<80%_of_your_main_memory><problem-file>

or

  eprover --satauto-schedule --memory-limit=<80%_of_your_main_memory><problem-file>

the prover will try a series of strategies on the problem. It assumesa 300 second run time - if you impose a different one externally, itis important to let E know via the--cpu-limit=XXX option so that itcan adjust the schedule. You can also enable usage of multiple coreswith the variant--auto-schedule=n (wheren is the number ofcores), or--auto-schedule=Auto to use all available cores.

One of the features of E is the ability to produce semi-readableproofs. To use this, type

  eprover --proof-object<other-stuff>

By default, E will now automatically detect the input format (LOP,TPTP-2 or TPTP-3), and will select the matching output format (PCL2for LOP and TPTP-2 inputs, TPTP-3 for TPTP-3 inputs).

You can check the proof objects in PCL format for correctness usingthe tool checkproof in the same directory. "checkproof -h" should giveyou all necessary information. Note that checkproof cannot yet dealwith the full first order part, and will skip anything notclausal. Also, support for independent provers in checkproof can besubject to bit-rot, as other systems and interfaces change.

We welcome bug reports and even reasonable questions. If the proverbehaves in an unexpected way, please include the followinginformation:

• What did you observe?
• What did you expect?
• The output ofeprover --version
• The full commandline that lead to the unexpected behaviour
• The input file(s) that lead to the unexpected behaviour

Most bug reports should be send toschulz@eprover.org. Bug reportswith respect to the HO-version should also be send tojasmin.blanchette@gmail.com. Please remember that this is an unpaidvolunteer service ;-).