Getting the Source Code for

READ THIS FIRST! :-)

lean is written in SICStus Prolog, but it works as well under Quintus Prolog (all warnings of the Quintus compiler can be ignored). It can easily be ported to other Prolog systems (some hints on porting it to other Prolog dialects can be found here).

There are at least five principle ways to get hold of the source code for lean:

  1. The old-fashioned way is that you get the paper and type the program off. This is also the the hardest way.

  2. The most fashionable way is that you just continue reading below and fetch the four individual files as the are mentioned in the text. This can be done by clicking on the corresponding file names; they all end with .pl and are typeset verbatim. (If you choose this, you are advised to save the files under the same names as they are mentioned in the text.)

  3. Another version is that you download a shell archive of about 18K containing the source code

    LeanTaPsrc.shar.

    You can do this now by just clicking on the file name above.

    Once you have the shell archive, unpack it as follows:

    lean comes in four Prolog files:

    1. leantest.pl defines four predicates which are supposed to be something like a user interface (see the paper for details):
      • provefml/1, the standard version of LeanTaP
      • incprovefml/1, the standard version using iterative deepening
      • uv_provefml/1, the version with universal variables
      • uv_incprovefml/1, the version with universal variables and iterative deepening.
      All these predicates get one argument, which is the name of a formula in the database. lean comes with a database of some of Pelletier's problems (see leantest.pl).

    2. The actual prover lives in leantap.pl and is defined as the predicates prove/2 and prove_uv/2. The program is poorly commented, but explained in detail in the paper.

    3. lean is restricted to formulas in Skolemized negation normal form. For your convenience, we included a program to translate formulas in this form: nnf.pl. Besides the tricky Skolemization we use (it is itself worth having a look), the program is routine. Again, all is explained in the paper.

    4. Last, but not least, you need a sound unification algorithm. Many Prolog systems do not provide this, but some do. If you have such a Prolog system, simply change the call to unify in leantap.pl accordingly. Otherwise, you need unify.pl (If I remember correctly, I "borrowed" this program a long time ago from Mark Stickel).

      (Most of the information above is also contained in the file README which also belongs to the standard distribution.)

      Once you have all the files, you can run lean. Here is an example.

      Maintainer: beckert@kit.edu