CMU Artificial Intelligence Repository
Home INFO Search FAQs Repository Root

LeanTaP: Tableau-based Theorem Prover for FOL

areas/reasonng/atp/systems/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 original LeanTaP program is only about 12 lines of Prolog: 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). 
See Also: 

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

Origin:   

   sonja.ira.uka.de:/pub/posegga/ [129.13.31.2]
   as the files LeanTaPsrc.shar.Z (source code) and
   LeanTaP.ps.Z (paper)
Version: 4-AUG-94 Requires: Sicstus Prolog or Quintus Prolog Copying: Copyright (c) 1993 by Bernhard Beckert and Joachim Posegga Universit"at Karlsruhe. Updated: Fri Oct 14 18:37:24 1994 CD-ROM: Mailing List: Send mail to the authors to be included in the mailing list for future developments of LeanTaP. Author(s): Bernhard Beckert Joachim Posegga Universit"at Karlsruhe Institut f"ur Logik, Komplexit"at und Deduktionssysteme Am Fasanengarten 5, 76128 Karlsruhe, FRG Phone: ++49 721 608 4322, Fax: ... 4329 Keywords: Authors!Beckert, Authors!Posegga, Automated Reasoning, FOL, First Order Logic, LeanTaP, Prolog!Code, Reasoning!Automated Reasoning, Tableau-Based Theorem Proving, Theorem Proving References: Bernhard Beckert and Joachim Posegga, "leanTaP: lean, tableau-based theorem proving", in Alan Bundy, editor, Proc. CADE-12, LNAI #814, Springer Verlag, Nancy, France, June/July 1994.
Last Web update on Mon Feb 13 10:27:33 1995
AI.Repository@cs.cmu.edu