# EKL—A Mathematically Oriented Proof Checker

## Abstract

EKL is an interactive theorem-proving system currently under development at the Stanford Artificial Intelligence Laboratory.

A version of EKL transportable to all TOPS-20 systems has been used for simple program verification tasks by students taking CS206, a LISP programmming course at Stanford.

The EKL project began in 1981 and has grown into a large and robust theorem-proving system within a relatively short span of time. It currently runs at SAIL (a KL10-based system at the Stanford Computer Science Department), comprising about 10000 lines of code written in MACLISP.

We describe some of the features of the language of EKL, the underlying rewriting system, and the algorithms used for high order unification. A simple example is given to show the actual operation of EKL.

## Keywords

Decision Procedure Type Ground Existential Quantifier Interactive Proof Conditional Branch## Preview

Unable to display preview. Download preview PDF.

## References

**Bledsoe, W. W.**,*Non-resolution Theorem-proving*, Artificial Intelligence 3, 1–36, 1977.MathSciNetCrossRefzbMATHGoogle Scholar**Boyer, R.S., Moore, J. S.**,*A computational logic*, Academic Press, New York, 1979.zbMATHGoogle Scholar**Boyer, R.S., Moore, J. S.**,*Metafunctions: Proving them correct and using them efficiently as new proof procedures*, SRI International, Technical Report CSL-108, 1979.Google Scholar**Bulnes, J.**,*Goal: a goal oriented command language for interactive proof construction*, Stanford AI Memo AIM-328, 1979.Google Scholar**de Bruijn, N.G.**,*AUTOMATH—A Language for Mathematics*, Technological University Eindhoven, Netherlands, 1968.zbMATHGoogle Scholar**Gabriel, R.P., Frost, M.E.**,*A Programming Environment for a Timeshared System*, to be presented at the 1984 Software Engineering Symposium on Practical Software Development Environments, 1984.Google Scholar**Gordon, M.J.C., Milner, R., Wadsworth, C.**,*Edinburgh LCF*, Springer-Verlag, New York, 1979.CrossRefzbMATHGoogle Scholar**Huet, G.P.**,*A unification Algorithm for Typed λ-Calculus*, Theoretical Computer Science 1, 27–57, 1975.MathSciNetCrossRefzbMATHGoogle Scholar**Jensen, D.C., Pietzrykowski, T.**,*Mechanizing ω-Order Type Theory Through Unification*, Theoretical Computer Science 3, 123–171, 1976.MathSciNetCrossRefGoogle Scholar**Jutting, L.S.**,*A translation of Landau’s “Grundlagen” in AUTOMATH*, Eindhovea University of Technology, Dept. of Math., 1976.Google Scholar**Ketonen, J., Weening, J.**,*EKL—An interactive proof checker*, Users’ Reference Manual, 40 pp., Stanford University, 1983.Google Scholar**Ketonen, J., Weening, J.**,*The Language of an Interactive Proof Checker*, 34 pp., Stanford University, CS Report STAN-CS-83-992, 1983.Google Scholar**Ketonen, J., Weyhrauch, R.**,*A semidecision procedure for predicate calculus*, 16 pp., to appear in the Journal of Theoretical Computer Science 1984.Google Scholar**Kreisel, G.**,*Neglected Possibilities of Processing Assertions and Proofs Mechanically: Choice of Problems and Data*, in University-Level Computer-Assisted Instruction at Stanford: 1968–1980, edited by Patrick Suppes, IMSSS, Stanford, 1981.Google Scholar**Lusk, E.L, McCune, W.W, Overbeek, R.A.**,*Logic Machine Architecture: Kernel functions*, in 6^{th}Conference on Automated Deduction, New York, edited by D.W. Loveland, Lecture Notes in Computer Science, No.138, Springer-Verlag, 70–84, 1982.Google Scholar**McCarthy, J.**,*Computer programs for checking mathematical proofs*, Proc. Symp. Pure Math., Vol. 5, American Mathematical Society, 219–227, 1962.CrossRefzbMATHGoogle Scholar**McCarthy, J., Talcott, C.**,*LISP: programming and proving*, to appear, available as Stanford CS206 Course Notes, Fall 1980.Google Scholar**Miller, D.A., Cohen, E., Andrews, P.B.**,*A look at TPS*, in 6^{th}Conference on Automated Deduction, New York, edited by D.W. Lovetand, Lecture Notes in Computer Science, No.138, Springer-Verlag, 70–84, 1982.Google Scholar**Shostak, R.E., Schwartz, R., Melliar-Smith, P.M.**,*STP: A Mechanized Logic for Specification and Verification*, in 6^{th}Conference on Automated Deduction, New York, edited by D.W. Loveland, Lecture Notes in Computer Science, No.138, Springer-Vertag, 32–49, 1982.Google Scholar**Weyhraueh, R.**,*Prolegomena to a theory of mechanized formal reasoning*, Stanford AI Memo AIM-315, 1978.Google Scholar**Wos, L.**,*Solving open questions with an automated theorem-proving program*, in 6^{th}Conference on Automated Deduction, New York, edited by D.W. Loveland, Lecture Notes in Computer Science, No.138, Springer-Verlag, 1–31, 1982.Google Scholar