---
title: "A Lemma Driven Automatic Theorem Prover for Recursive Function Theory"
authors:
  - "Robert S. Boyer"
  - "J. Strother Moore"
doi: ""
url: "https://ijcai.org/proceedings/1977/117"
pdf: "https://ijcai.org/proceedings/1977/0117.pdf"
venue: "Proceedings of the Fifth International Joint Conference on Artificial Intelligence"
year: 1977
pages: "511-518"
track: "Theorem Proving"
keywords:
---

# A Lemma Driven Automatic Theorem Prover for Recursive Function Theory

Robert S. Boyer, J. Strother Moore

*Proceedings of the Fifth International Joint Conference on Artificial Intelligence*, pages 511-518.

## Abstract

We describe work in progress on an automa tic theorem prover for recursive function theory that we intend to apply in the analysis (including verification and transformation) of useful computer programs. The mathematical theory of our theorem prover is extendible by the user and se rves as a logical basis of program specification (ana logous 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. We descr i be several ways that the theorem prover employs such lemmas. Among the interesting theorems proved are the correctness of a simple optimizing compiler for expressions and the correctness of a "big number" addition algorithm. The research reported here has been supported by the Office of Naval Research under Contract N00014-75-C-0816, the National Science Foundation under Grant DCR72-03737A01, and the Air Force Office of Scientific Research under Contract F44620-73-C-0068.