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.
Research supported by NSF grant MCS-82-06565 and ARPA contract N00039-82-C-0250.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bledsoe, W. W., Non-resolution Theorem-proving, Artificial Intelligence 3, 1–36, 1977.
Boyer, R.S., Moore, J. S., A computational logic, Academic Press, New York, 1979.
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.
Bulnes, J., Goal: a goal oriented command language for interactive proof construction, Stanford AI Memo AIM-328, 1979.
de Bruijn, N.G., AUTOMATH—A Language for Mathematics, Technological University Eindhoven, Netherlands, 1968.
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.
Gordon, M.J.C., Milner, R., Wadsworth, C., Edinburgh LCF, Springer-Verlag, New York, 1979.
Huet, G.P., A unification Algorithm for Typed λ-Calculus, Theoretical Computer Science 1, 27–57, 1975.
Jensen, D.C., Pietzrykowski, T., Mechanizing ω-Order Type Theory Through Unification, Theoretical Computer Science 3, 123–171, 1976.
Jutting, L.S., A translation of Landau’s “Grundlagen” in AUTOMATH, Eindhovea University of Technology, Dept. of Math., 1976.
Ketonen, J., Weening, J., EKL—An interactive proof checker, Users’ Reference Manual, 40 pp., Stanford University, 1983.
Ketonen, J., Weening, J., The Language of an Interactive Proof Checker, 34 pp., Stanford University, CS Report STAN-CS-83-992, 1983.
Ketonen, J., Weyhrauch, R., A semidecision procedure for predicate calculus, 16 pp., to appear in the Journal of Theoretical Computer Science 1984.
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.
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.
McCarthy, J., Computer programs for checking mathematical proofs, Proc. Symp. Pure Math., Vol. 5, American Mathematical Society, 219–227, 1962.
McCarthy, J., Talcott, C., LISP: programming and proving, to appear, available as Stanford CS206 Course Notes, Fall 1980.
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.
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.
Weyhraueh, R., Prolegomena to a theory of mechanized formal reasoning, Stanford AI Memo AIM-315, 1978.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1984 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ketonen, J. (1984). EKL—A Mathematically Oriented Proof Checker. In: Shostak, R.E. (eds) 7th International Conference on Automated Deduction. CADE 1984. Lecture Notes in Computer Science, vol 170. Springer, New York, NY. https://doi.org/10.1007/978-0-387-34768-4_4
Download citation
DOI: https://doi.org/10.1007/978-0-387-34768-4_4
Publisher Name: Springer, New York, NY
Print ISBN: 978-0-387-96022-7
Online ISBN: 978-0-387-34768-4
eBook Packages: Springer Book Archive