Proving Theorems about LISP Functions
Proceedings of the Third International Joint Conference on Artificial Intelligence. Automatic Programming. 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.
Robert S. Boyer, and J. Strother Moore. 1973. Proving Theorems about LISP Functions. In Proceedings of the Third International Joint Conference on Artificial Intelligence, IJCAI-73. IJCAI, 486–492. https://ijcai.org/proceedings/1973/62
Boyer, R. S., & Moore, J. S. (1973). Proving Theorems about LISP Functions. In Proceedings of the Third International Joint Conference on Artificial Intelligence, IJCAI-73 (pp. 486–492). IJCAI. https://ijcai.org/proceedings/1973/62
@inproceedings{ijcai1973p62,
title = {Proving Theorems about LISP Functions},
author = {Boyer, Robert S. and Moore, J. Strother},
booktitle = {Proceedings of the Third International Joint Conference on
Artificial Intelligence, {IJCAI-73}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Nils J. Nilsson},
pages = {486--492},
year = {1973},
month = {8},
note = {Automatic Programming},
url = {https://ijcai.org/proceedings/1973/62},
}
TY - CPAPER TI - Proving Theorems about LISP Functions AU - Boyer, Robert S. AU - Moore, J. Strother T2 - Proceedings of the Third International Joint Conference on Artificial Intelligence, IJCAI-73 PB - International Joint Conferences on Artificial Intelligence PY - 1973 SP - 486 EP - 492 UR - https://ijcai.org/proceedings/1973/62 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
