Report Number: CS-TR-83-992
Institution: Stanford University, Department of Computer Science
Title: The language of an interactive proof checker
Author: Ketonen, Jussi
Author: Weening, Joseph S.
Date: December 1983
Abstract: We describe the underlying language for EKL, an interactive
theorem-proving system currently under development at the
Stanford Artificial Intelligence Laboratory. Some of the
reasons for its development as well as its mathematical
properties are discussed.