leanTAP Theorem Prover

Appeared in Volume 7/4, November 1994

Keywords: theorem provers.

This is to announce the creation of a leanTAP mailing list and leanTAP WWW pages. If you want to be included in the mailing list, drop one of us a line. The URL for the leanTAP home page is:

http://i12www.ira.uka.de/~posegga/leantap/leantap.html

leanTAP is a complete and sound theorem prover for classical first-order logic based on free-variable semantic tableaux written in Prolog. The unique thing about leanTAP is that it is probably the smallest theorem prover around. The minimal version of the Prolog source code is only 360 bytes.

If you do not have access to the World Wide Web, you can get the leanTAP source code and the documentation via FTP from:
ftp://sonja.ira.uka.de/pub/posegga/
Get all the files with names of the form "Lean*".

Bernhard Beckert, Joachim Posegga
Universitaet Karlsruhe
Institut fuer Logik, Komplexitaet und Deduktionssysteme
Am Fasanengarten 5 
76128 Karlsruhe, Germany 
Email: posegga@ira.uka.de, 
       beckert@ira.uka.de
Tel: +49 721 608 4324 or 4322
Fax: +49 721 608 4329