		Search-engine friendly clone of the ACL2 documentation.

Operational-semantics-3__annotated-bibliography

Bib::bm73

R. S. Boyer and J S. Moore, “Proving Theorems about LISP Functions”, in Proceedings of the Third International Joint Conference on Artificial Intelligence (IJCAI), Stanford University, pp. 486-493, 1973.

Relevance: journal article about the Edinburgh Pure Lisp Theorem Prover (PLTP)

———

For a longer, journal version of this paper see R. S. Boyer and J S. Moore, “Proving Theorems about LISP Functions”, Journal of the ACM, 22(1), pp. 129-144, 1975.

The IJCAI'73 paper was the first widely accessible description of the Edinburgh Pure Lisp Theorem Prover (PLTP). The key ideas in the theorem prover were the use of Lisp as a logic, the reliance on recursive function definitions, extensive use of rewriting and symbolic evaluation, and an induction heuristic based on the failure of symbolic evaluation. The system was fully automatic; there were no provisions for user supplied lemmas or hints.

The “proveall” (regression suite) included such theorems as associativity of append, reverse-reverse, and the correctness of insertion sort. The paper was hailed as a landmark in theorem proving because these theorems had never been proved automatically before. But early critics said that proving theorems about pure Lisp was irrelevant because serious applications were not written in pure Lisp. However, Boyer and Moore argued that Lisp was a logic with features necessary to the specification and proof of program properties, namely recursive definitions and mathematical induction.

The PLTP Archive contains a wealth of information about PLTP and its 1973 implementation in POP-2, including the POP-2 Reference Manual, scanned OCR listings of the PLTP source code, listings of proof output, and modern reconstructions of PLTP in OCaml (by Grant Passmore) and ACL2 (by J Moore).