EKL—A Mathematically Oriented Proof Checker
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.
KeywordsDecision Procedure Type Ground Existential Quantifier Interactive Proof Conditional Branch
Unable to display preview. Download preview PDF.
- 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
- 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
- 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 6th 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., 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 6th 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 6th 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 6th 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