---
title: "Proving Theorems about LISP Functions"
authors:
  - "Robert S. Boyer"
  - "J. Strother Moore"
doi: ""
url: "https://ijcai.org/proceedings/1973/62"
pdf: "https://ijcai.org/proceedings/1973/0062.pdf"
venue: "Proceedings of the Third International Joint Conference on Artificial Intelligence"
year: 1973
pages: "486-492"
track: "Automatic Programming"
keywords:
---

# Proving Theorems about LISP Functions

Robert S. Boyer, J. Strother Moore

*Proceedings of the Third International Joint Conference on Artificial Intelligence*, pages 486-492.

## Abstract

e desc r ibe some simple heu ri stics combining evaluatio n and mathematical induction which we have implemented in a program that a utomatically proves a wide va riety of theorems a bout recursive LISP functions . The method the program uses to gene r ate induction formulas is described at l ength . The theorems proved by the progr am include that REVERSE is its own inverse and that a pa rti c ular SORT program is correct . Appendix B contains a list of the t he orems proved by the program.