: 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 :

The best paper to read on lean is (PDF):
The paper is 20 pages long; it contains a sketch of a proof for lean's correctness and completeness, and a brief historical survey on tableau-based provers (BibTeX entry).
The chapter on implementing semantic tableaux (PDF) of the Handbook of Tableau-based Methods in Automated Deduction to be published by Kluwer Academic Publishers. The chapter has been written by Joachim Posegga and Peter H. Schmitt; it describes lean and similar Prolog implementations.
A short version (PDF; BibTeX) of the paper that appeared in the Journal of Automated Reasoning was presented at CADE-12 in Nancy. It has 5 pages and might be good for a quick introduction. However, it is does not tell the whole story.
The lean-FAQ (PDF). If you have any questions regarding lean and cannot find the answers in the above long paper, you probably find it here. But even if you do not have any particular questions, you will find a lot of interesting information.
Furthermore, there are two short position papers on the idea of lean deduction:
- The first paper (PDF; BibTeX) has been presented at the AISB Workshop Automated Reasoning: Closing the Gap between Theory and Practice in Leeds, England.
- The second one (PDF; BibTeX) has been presented at the Logic Programming Workshop in Zürich, Switzerland.
And finally, there is a paper by Joachim Posegga (PDF) on the working principle of the lean Compiler. This is a variant of lean which performs a compilation-based proof search (like Stickels PTTP, but not restricted to CNF). This compiler, which is a lean-style program (well, to be honest: the compiler is about 25 lines long), is stable but the paper describing it remains to be written...

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).

A format file is available for converting problems taken from the TPTP library 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:

Bernhard Beckert
Karlsruhe Institute of Technology
Email: beckert@kit.edu

Joachim Posegga
University of Passau
Email: posegga@uni-passau.de

INDEX: what is leanTAP? papers source code contact address

Maintainer: Bernhard Beckert