ML Anthology

Proving Theorems About LISP Functions

Robert S. Boyer, J Strother Moore
IJCAI 1973 pp. 486-493
doi:10.1145/321864.321875 /ijcai/1973/boyer1973ijcai-proving/

Abstract

Program verication is the idea that properties of programs can be precisely stated and proved in the mathematical sense. In this paper, some simple heuristics combining evaluation and mathematical induction are described, which the authors have implemented in a program that automatically proves a wide variety of theorems about recursive LISP functions. The method the program uses to generate induction formulas is described at length. The theorems proved by the program include that REVERSE is its own inverse and that a particular SORT program is correct. A list of theorems proved by the program is given. key words and phrases: LISP, automatic theorem-proving, structural induction, program verication cr categories: 3.64, 4.22, 5.21 1

PDF Semantic Scholar

Cite

Text

Boyer and Moore. "Proving Theorems About LISP Functions." International Joint Conference on Artificial Intelligence, 1973. doi:10.1145/321864.321875

Markdown

[Boyer and Moore. "Proving Theorems About LISP Functions." International Joint Conference on Artificial Intelligence, 1973.](https://mlanthology.org/ijcai/1973/boyer1973ijcai-proving/) doi:10.1145/321864.321875

BibTeX

@inproceedings{boyer1973ijcai-proving,
  title     = {{Proving Theorems About LISP Functions}},
  author    = {Boyer, Robert S. and Moore, J Strother},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {1973},
  pages     = {486-493},
  doi       = {10.1145/321864.321875},
  url       = {https://mlanthology.org/ijcai/1973/boyer1973ijcai-proving/}
}