The title of this paper is slightly misleading and the misunderstanding is corrected in the very first line. EKL is an interactive theorem-proving system currently under development at the Stanford University AI Laboratory. It is intended to be used in situations when the user (thinks he) knows well not only the goal to be proved, but almost all details of the proof. Most theorem provers of the previous decade have been based on the unrestricted generation of new consequences or subgoals by the program governed only by some strategy fixed before execution. The trend now is obviously in the direction of interactive user-directed proof-construction with much less space and time for purely mechanical search.
EKL seems to be an extreme expression of this trend: only depth one (or sometimes two) search is allowed except for rewriting or special proof procedure for easily decidable subcase of the predicate logic. For example, it can use higher-order induction but no induction heuristics; in many cases, one has to specify the instances of induction used. Most of the burden of the theorem-proving is taken by the rewriting (simplification) process. The main aim is to imitate actual mathematical practice by creating a system and a language which would allow the expression and verification of mathematical facts in a direct, readable, and natural way. The language consists of finite-order predicate logic with typed lambda-calculus, and a decidable restriction of (undecidable in general) higher-order unification is used. The emphasis is on introducing and using the definitions of new notions. As a successful example, the author points out an elegant 50-line proof of Ramsey’s theorem he has been able to produce (the shortest computer-checked proof previously known was above 400 lines). This is not so convincing after one recalls that the author is the coauthor of a very deep proof-theoretic analysis of Ramsey-type theorems. Projected comparative study of EKL and AUTOMATH proofs of theorem in Landau’s Grundlagen may be more informative.
