### CLIB-0.2 README file

    This is the README file for version 0.2 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!

    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 then there are games within
    EMACS...

    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 programst. While I try to keep new features useful
    for other purposes, this direction determines which features I myself
    will add.

    CLIB has been created and is currently maintained by Stephan Schulz,
    <schulz@informatik.tu-muecnchen.de>.

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

    To install the package, unpack the distribution with "gunzip
    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. Type "make
    documentation" to translate the rudimentary LaTeX documentation. For
    some operating systems, you may need to edit Makefile.vars to select
    tools and options.

    Go to CLIB/PROVER and type "./eprover BOO006_2.lop" to see the
    prover in action. Type "./eprover BOO007-2+rm_eq_rstfp.lop" if you
    are patient.

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

    DOC:

      - Documentation, including a LaTeX manual for (at the moment) parts
        of the library. 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,...

    EXAMPLES:

      - Example problems (unit-equality specifications) taken from the
        TPTP 2.1.0 library.