Portal de Periódicos da CAPES

EKL—A Mathematically Oriented Proof Checker

1984; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-0-387-34768-4_4

1611-3349

Jussi Ketonen,

Software Testing and Debugging Techniques

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.