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

EKL has recently (November 1981) undergone rather major changes.  To get
functions which simulate TAUT, DECSIMP, the old REWRITE, etc. (which no
longer exist), give EKL the command

	(FASLOAD (DSK (EKL JK)) FIX FAS)

or include such a line in your EKL.INI file.

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