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.