: Lean, Tableau-based Deduction

INDEX: what is leanTAP? papers source code contact address
This is the home page of lean, a complete and sound theorem prover for first-order logic.

What is ?

lean was invented by Bernhard Beckert and Joachim Posegga. It is written in Prolog and implements a complete and sound theorem prover for classical first-order logic based on free-variable semantic tableaux. The unique thing about lean is that it is probably the smallest theorem prover around.

The minimal version of the Prolog source code is only 360 bytes. This is of course hardly readable; there is also the standard distribution of lean, which comes with a rudimentary user interface and some test examples. It is distributed as a shell archive (see information on getting the source code).

In addition, there is a lean tableau-based prover available for propositional modal logics, called ModLeanTAP.

Jens Otten from TU Darmstadt has developed a lean connection-based prover leanCoP. There is also a version for intuitionistic first-order logics, called ileanTAP.

Papers on :

Source Code for

See this speparate document on how to get the source code.

lean is written in SICStus Prolog, but it works as well under Quintus Prolog, and it can be easily ported to other Prolog systems (for example Eclipse and SWI Prolog).

Problems taken from the TPTP library can be converted into lean syntax (using the program tptp2x, which is part of the TPTP distribution).

Please Contact Us

Do not hesitate to contact us if you are looking for any information you cannot find on these pages, or should you have any further questions, suggestions, or comments.

Finally, if should you do something interesting with lean, please inform us. This could be modifying or extending the program, applying it to some domain, or whatever. We appreciate feedback.

Contact address:

INDEX: what is leanTAP? papers source code contact address
Maintainer: Bernhard Beckert