A Lemma Driven Automatic Theorem Prover for Recursive Function Theory

Abstract

The paper describes work in progress on an automatic theorem prover for recursive function theory that is intended to be applied in the anlaysis (including verification and transformation) of useful computer programs. The mathematical theory of the theorem prover is extendible by the user and serves as a logical basis of program specification (analogous to, say, the predicate calculus). The theorem prover permits no interaction once given a goal, but many aspects of its behavior are influenced by previously proved results. Thus, its performance on difficult theorems can be radically improved by having it first prove relevant lemmas. The theorem prover employs such lemmas in several ways. Among the interesting theorems proved are the correctness of a simple optimizing compiler for expressions and the correctness of a 'big number' addition algorithm.