This is the README file for version 0.63 "Nuwara Eliya" of the E equational theorem prover. This version of E is free software, see the file COPYING for details about the license and the fact that THERE IS NO WARRANTY! If you are interested in a proprietary version of E with support, see below. Release 0.63 is a minor release, mainly to offer a stable basis for major changes. For changes see DOC/NEWS If you are using gcc 2.95.1, 2.96.X or 2.97.X, 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. In fact, E and CLIB are now so intertwined that you will not find a pure CLIB anymore. CLIB and E have been created and are currently maintained by Stephan Schulz, . They are developed and distributed under the GNU General Public License. However, you may possibly come around versions sold or given to you under a different license sold to Safelogic A.B. in Gothenburg, Sweden. Safelogic bought the right to distribute (and relicense) closed-source versions of E with proprietary modifications. If you are interested in their modifications, want a proprietary version with support, or want to relicense a modified version under a non-GPL license, you can contact them at johan.alfredsson@safelogic.se. 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 (if you are reading this, 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, edit E/Makefile.vars to your liking. In particular, if building for HPUX, comment out the suitable CFLAGS definition (for most systems, the default definition should be ok). cd E make install to compile and install the library and all included programs under the E directory. If you want to use the prover "eprover" and the wrapper script "eproof" anywhere except in the E/PROVER directory, set the EXECPATH variable in Makefile.vars to a suitable directory and type make install-exec 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 E/DOC/PORTING. After installation, go to E/PROVER and type ./eprover BOO001-1+rm_eq_rstfp.lop to see the prover in action. Type ./eprover BOO007-2+rm_eq_rstfp.lop for a harder example. "./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> 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 | e2pcl or use the wrapper-script eproof problem You can check the output of e2pcl (and eproof) 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: ANALYSIS: HEURISTICS: PCL2: 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.