Advertisement

EKL—A Mathematically Oriented Proof Checker

  • Jussi Ketonen
Part of the Lecture Notes in Computer Science book series (LNCS, volume 170)

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 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bledsoe, W. W., Non-resolution Theorem-proving, Artificial Intelligence 3, 1–36, 1977.MathSciNetCrossRefzbMATHGoogle Scholar
  2. Boyer, R.S., Moore, J. S., A computational logic, Academic Press, New York, 1979.zbMATHGoogle Scholar
  3. 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
  4. Bulnes, J., Goal: a goal oriented command language for interactive proof construction, Stanford AI Memo AIM-328, 1979.Google Scholar
  5. de Bruijn, N.G., AUTOMATH—A Language for Mathematics, Technological University Eindhoven, Netherlands, 1968.zbMATHGoogle Scholar
  6. 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
  7. Gordon, M.J.C., Milner, R., Wadsworth, C., Edinburgh LCF, Springer-Verlag, New York, 1979.CrossRefzbMATHGoogle Scholar
  8. Huet, G.P., A unification Algorithm for Typed λ-Calculus, Theoretical Computer Science 1, 27–57, 1975.MathSciNetCrossRefzbMATHGoogle Scholar
  9. Jensen, D.C., Pietzrykowski, T., Mechanizing ω-Order Type Theory Through Unification, Theoretical Computer Science 3, 123–171, 1976.MathSciNetCrossRefGoogle Scholar
  10. Jutting, L.S., A translation of Landau’s “Grundlagen” in AUTOMATH, Eindhovea University of Technology, Dept. of Math., 1976.Google Scholar
  11. Ketonen, J., Weening, J., EKL—An interactive proof checker, Users’ Reference Manual, 40 pp., Stanford University, 1983.Google Scholar
  12. Ketonen, J., Weening, J., The Language of an Interactive Proof Checker, 34 pp., Stanford University, CS Report STAN-CS-83-992, 1983.Google Scholar
  13. Ketonen, J., Weyhrauch, R., A semidecision procedure for predicate calculus, 16 pp., to appear in the Journal of Theoretical Computer Science 1984.Google Scholar
  14. 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
  15. 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
  16. McCarthy, J., Computer programs for checking mathematical proofs, Proc. Symp. Pure Math., Vol. 5, American Mathematical Society, 219–227, 1962.CrossRefzbMATHGoogle Scholar
  17. McCarthy, J., Talcott, C., LISP: programming and proving, to appear, available as Stanford CS206 Course Notes, Fall 1980.Google Scholar
  18. 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
  19. 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
  20. Weyhraueh, R., Prolegomena to a theory of mechanized formal reasoning, Stanford AI Memo AIM-315, 1978.Google Scholar
  21. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • Jussi Ketonen
    • 1
  1. 1.Stanford UniversityUSA

Personalised recommendations