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.
http://i.stanford.edu/pub/cstr/reports/cs/tr/84/1006/CS-TR-84-1006.pdf