The project EKL at Stanford Artificial Intelligence Laboratory was initiated by
Jussi Ketonen and John McCarthy at the beginning of the 1980s, building on
the experience of Richard Weyhrauch's theorem prover FOL. EKL is a LISP
program, designed for an efficient representation of mathematical proofs
and for a versatile use in program verifiaction. Features of EKL are:
- typed language;
- higher order rewriting, based upon G.Huet's higher order unification
- a decision procedure for a fragment of first order logic, called Direct
Logic, known today as Affine Logic, i.e., Multiplicative Linear Logic with
EKL was written around 1980. From 1980 to 1984 EKL was used in the following projects:
- partial formalization of Landau's Foundations of Analysis;
- proofs of specifications and of correctness of LISP programs;
see Bellin and Ketonen, 1987.
- an implementation of the functional interpretation of the infinite Ramsey
theorem. More precisely, a higher order automated proof of the infinite
Ramsey theorem has been rewritten it in first order logic and then
Kreisel's No Counterexample Interpretation has been applied to it.
See Bellin 1990.
- the theoretical aspects of the EKL decision procedure and its relations
with Girard's linear logic have been thoroughly investigated between 1986 and
1990, see Bellin and Ketonen, 1992.
Further documentation on EKL:
A Type System for a Mechanized Logic,
preprint, Computer Science Department, Stanford University, 1983.
EKL-A Mathematically Oriented Proof Checker,
Proceedings of the Seventh Conference on Automated Deduction,
Lecture Notes in Computer Science 170, pp.65-79
- J.Ketonen and J.S.Weening. The Language of an Interactive
Report No. STAN-CS-83-992 Computer Science Department,
- J.Ketonen and J.S.Weening. EKL-An Interactive Proof Checker
User's Reference Manual
Computer Science Department, Stanford University.
- J.Ketonen and R.Weyhrauch, 1984. A Decidable Fragment of the
Theoretical Computer Science 32 (1984),