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