From beckert@i12s1.ira.uka.de Wed Aug 10 19:42:15 EDT 1994 Article: 11012 of comp.lang.prolog Path: cantaloupe.srv.cs.cmu.edu!nntp.club.cc.cmu.edu!newsfeed.pitt.edu!gatech!newsxfer.itd.umich.edu!zip.eecs.umich.edu!yeshua.marcam.com!usc!math.ohio-state.edu!jussieu.fr!univ-lyon1.fr!swidir.switch.ch!scsing.switch.ch!xlink.net!news.urz.uni-heidelberg.de!rz.uni-karlsruhe.de!i12s1!beckert From: beckert@i12s1.ira.uka.de (Bernhard Beckert) Newsgroups: sci.logic,comp.lang.prolog Subject: leanTAP theorem prover Date: 4 Aug 1994 14:56:00 GMT Organization: University of Karlsruhe, FRG Lines: 80 Sender: beckert@i12s1 (Bernhard Beckert) Distribution: world Message-ID: <31qvi0$2pc@nz12.rz.uni-karlsruhe.de> NNTP-Posting-Host: i12s1.ira.uka.de Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit Xref: glinda.oz.cs.cmu.edu sci.logic:7764 comp.lang.prolog:11012 T h e @@@ @ @@ @@ @ @@@@@@@@ @@ @@ @@@@@@@@ @ @@@ @@@ @ @@ @ @@ @ @@ @@ @@ @@ @ @ @ @ @@ @ @@ @@@@@@@@ @@ @@ @ @@@@@ @@@@ @ @ @@ @@ @@ @@@@@@@ @ @ @ @@ @ @ @@ @@ @@ @@ @ @ @ @@ @ @ @@ @@ @@@ @@@ @@ @@ @ @ @@@@ @@@@ M a i l i n g - L i s t and W o r l d W i d e W e b P a g e s +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 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 (beckert@ira.uka.de or posegga@ira.uka.de). The URL for the leanTAP home page is: http://i12www.ira.uka.de/~posegga/leantap/leantap.html + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Some information on leanTAP: 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: prove((E,F),A,B,C,D) :- !,prove(E,[F|A],B,C,D). prove((E;F),A,B,C,D) :- !,prove(E,A,B,C,D),prove(F,A,B,C,D). prove(all(I,J),A,B,C,D) :- !, \+length(C,D),copy_term((I,J,C),(G,F,C)), append(A,[all(I,J)],E),prove(F,E,B,[G|C],D). prove(A,_,[C|D],_,_) :- ((A= -(B);-(A)=B) -> (unify(B,C);prove(A,[],D,_,_))). prove(A,[E|F],B,C,D) :- prove(E,F,[A|B],C,D). This is of course hardly readable; there is also a standard distribution of leanTAP, which comes with a rudimentary user interface and some test examples. If you do not have access to the World Wide Web, you can get the leanTAP source code and the documentation via FTP from sonja.ira.uka.de (129.13.31.2). Look into the directory pub/posegga/ and get all the files with names of the from "Lean*". A short description of leanTAP 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. Bernhard Beckert -- 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 Phone: Bernhard: ++49 (0)721 608 4324, Joachim: ... 4322 Fax: ++49 (0)721 608 4329