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].
(Note: this manual is currently not up to date.)
For less complete online documentation, see EKL.MAN[EKL,JK].

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

EKL has recently (November 1981) undergone rather major changes.  To
use the version which existed before November 20, 1981, say

	.run okl[ekl,jk]

to the monitor.  To get functions which simulate TAUT, DEC, 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.