EKL is a programmable interactive proof checker and constructor.
It is written in MACLISP.

You can spool yourself a manual by typing DOVER EKLMAN.PRE[EKL,JJW].
For less complete online documentation, see EKL.MAN[EKL,JK].

The manual for the old version of EKL (which is still in use at SCORE
and LOTS) is on EKLOLD.PRE[EKL,JJW].