This is the README file for version 0.61 "North Tukvar" of the E
equational theorem prover. E is free software, see the file COPYING
for details about the license and the fact that THERE IS NO WARRANTY!

Release 0.61 is a intermediate release. Very much new stuff has been
added and should work fine, however, the documentation of many new
features is still lacking.

If you are using gcc 2.95.1, please read DOC/PORTING for important
information. 


What is E? What is CLIB?
------------------------

E is an equational theorem prover. That means it is a program that you
can stuff a mathematical specification (in clausal logic with
equality) and a hypothesis into, and which will then run forever,
using up all of your machines resources. Very occasionally it will
find a proof for the hypothesis and tell you so ;-).

CLIB is a collection of library functions for building one class of
interesting and cool programs. Interesting and cool programs read a
specification file (or multiple files), process the input, and print a
result, or they are games. Examples for cool and interesting programs
are DISCOUNT (a distributed theorem prover), proof (a proof
transformation tool), DOOM (a game) and xevil (also a game). The sole
exception to this rule is EMACS, which is interesting and cool despite
being interactive and not a game. But it has a LISP interpreter, which
is very much like a game....

At the moment CLIB is more suited for theorem provers and similar
programs, and less useful for games. This will probably change as soon
as the game potential of theorem provers is recognized ;-)

CLIB is layered, with higher layers becoming more specialized. Lower
levels take care of the scientifically uninteresting, but necessary
services for production-quality efficient programs, e.g. error
handling, memory management, parsing of input, etc. They should be
useful for most programs (even for some interactive programs).

Higher level modules implement shared and unshared terms, equations,
clauses and related stuff.

My aim in writing this library is to ease the development of E and a
couple of auxiliary programs. While I try to keep new features useful
for other purposes, this direction determines which features I myself
will add.

CLIB and E have been created and are currently maintained by Stephan
Schulz, <schulz@informatik.tu-muenchen.de>.


Installation:
-------------

E can be installed anywhere in the file system, either by a normal
user or by the system administrator.

To install the package, unpack the distribution with "gunzip -c
CLIB.tgz|tar -xvf -" (or "tar -xzf CLIB.tgz" if you have GNU
tar). This should create a directory named CLIB. After unpacking,
"make install" in the CLIB directory should compile and install the
library and all included programs (all under the CLIB directory). Type
"make documentation" to translate the rudimentary LaTeX documentation
(this requires LaTeX2e and the packages theorem, amssymb and epsfig,
which are included in most current LaTeX distributions). For some
operating systems, especially if you do not have the GNU gcc compiler
installed, you may need to edit Makefile.vars to select tools and
options. If you have any problems, look into CLIB/DOC/PORTING.

After installation, go to CLIB/PROVER and type 

./eprover BOO001-1+rm_eq_rstfp.lop

to see the prover in action. Type 

./eprover BOO007-2+rm_eq_rstfp.lop

if you are patient. "./eprover -h" will give you some information and
a list of options.

For impatient people who do not want to read anything: 

eprover -tAuto -xAuto --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).

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

eprover -l4 <other-stuff> | e2pcl

You can check the output of e2pcl for correctness using the tool
checkproof in the same directory. "checkproof -h" should give you all
necessary information.


Directory overview:
-------------------

DOC:


  - Documentation, including a very preliminary LaTeX manual for (at
    the moment) parts of the library and the prover. You should be
    looking there instead of reading this file ;-)

    Also has the project HISTORY file and some short notes on
    porting.

include:

  - Symbolic links to all user-relevant header files

lib:

  - Symbolic links to the individual library modules

BASICS:
INOUT:
TERMS:
ORDERINGS:
CLAUSES:
HEURISTICS:
CONTROL:

  - Sources and object files for the individual library modules

TEST:

  - Test programs for development work

SIMPLE_APPS:

  - Small application programs for demonstration purposes as well as
    for solving simple tasks.

PROVER:

  - The main program for the E prover, also contains some examples and
    stuff.

SKELETONS:

  - Skeleton files for source files, make files, comment boxes,...


EXAMPLE_PROBLEMS:

  - Example problems taken from the TPTP 2.1.0 library.

EXTERNAL:

  - Code that does not belong to the core prover but uses it or parts
    of it. Not fully maintained by me, check the headers.