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:
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:
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: firstname.lastname@example.org, email@example.com Tel: +49 721 608 4324 or 4322 Fax: +49 721 608 4329