Report Number: CS-TR-84-1006
Institution: Stanford University, Department of Computer Science
Title: EKL - an interactive proof checker user's reference manual
Author: Ketonen, Jussi
Author: Weening, Joseph S.
Date: June 1984
Abstract: EKL is an interactive proof checker and constructor. Its main
goal is to facilitate the checking of mathematical proofs.
Some of the special features of EKL are:
* The language of EKL can be extended all the way to
finite-order predicate logic with typed lambda-calculus.
* Several proofs can be handled at the same time.
* Metatheoretic reasoning allows formal extensions of the
capabilities of EKL.
* EKL is a programmable system. The MACLISP language is
available to the user, and LISP functions can be written to
create input to EKL, thereby allowing expression of proofs in
an arbitrary input language.
This document is a reference manual for EKL. Each of the
sections discusses a major part of the language, beginning
with an overview of that area, and proceeding to a detailed
discussion of available features. To gain an acquaintance
with EKL, it is recommended that you read only the
introductory part of each section.
EKL may be used both at the Stanford Artificial Intelligence
Laboratory (SAIL) computer system, and on DEC TOPS-20 systems
that support MACLISP.