Automated Deduction

A Genealogy of Theorem Provers

FOL (First Order Logic) A general-purpose LISP-based theorem-prover. Richard Weyhrauch et al., 1975-

EKL (``First Order Logic'' in Finnish) A mathematically oriented LISP-based proof-checker. Jussi Ketonen et al., 1980-

Verona (A new project at the University of Verona) A JAVA-based program that recognizes and transforms abstract syntax, 1998-

Look here for an implementation of the trips by Jacques van de Wiele, an algorithm that yields a linear lambda term, given any pointed graph where all vertices have incidence 1 or 3.

pointed graph: a graph with a selected external vertex of incidence 1.

back home