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].