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:
.pland 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.)
You can do this now by just clicking on the file name above.
Once you have the shell archive, unpack it as follows:
% sh LeanTaPsrc.shar x - extracting README (Text) x - extracting leantap.pl (Text) x - extracting leantest.pl (Text) x - extracting nnf.pl (Text) x - extracting unify.pl (Text)
lean comes in four Prolog files:
leantest.pldefines 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.
leantap.pland is defined as the predicates prove/2 and prove_uv/2. The program is poorly commented, but explained in detail in the paper.
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.
leantap.placcordingly. 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.