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 algorithm;

• a decision procedure for a fragment of first order logic, called Direct Logic, known today as Affine Logic, i.e., Multiplicative Linear Logic with unrestricted Weakening.

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:

• J.Ketonen. A Type System for a Mechanized Logic,
  preprint, Computer Science Department, Stanford University, 1983.

• J.Ketonen. EKL-A Mathematically Oriented Proof Checker,
  Proceedings of the Seventh Conference on Automated Deduction, (Shostak ed.)
  Lecture Notes in Computer Science 170, pp.65-79

• J.Ketonen and J.S.Weening. The Language of an Interactive Proof Checker
  Report No. STAN-CS-83-992 Computer Science Department, Stanford University.

• J.Ketonen and J.S.Weening. EKL-An Interactive Proof Checker User's Reference Manual
  Report No.STAN-CS-84-1006, Computer Science Department, Stanford University.

• J.Ketonen and R.Weyhrauch, 1984. A Decidable Fragment of the Predicate Calculus
  Theoretical Computer Science 32 (1984), pp.297-307.

back home