PLTP(A): An ACL2 Implementation of the Edinburgh Pure Lisp Theorem Prover of 1973

J Strother Moore
March, 2018


This directory contains a contemporary (2017) implementation of PLTP coded in the applicative (functional) Common Lisp of ACL2. We name this system PLTP(A). PLTP(A) is almost a translation into ACL2 of the 14 September, 1973, listing of the POP-2 for PLTP. We explain the differences below. The material here is organized as follows. First we summarize the main files posted here so you can (i) browse the ACL2 source code for PLTP(A), (ii) inspect PLTP(A)'s standard proveall and JACM proveall, including the output of PLTP(A) on those regression suites, and (iii) read our argument that the two failures in its standard proveall do not indicate a discrepancy between PLTP and PLTP(A). Next, we describe the differences between the original PLTP and PLTP(A). The differences include bug fixes and some ``gratuitous'' changes to make the new code clearer. Finally, we explain how to get ACL2 and how to run PLTP(A).

Browsing PLTP(A)

Note: If you intend to run PLTP(A) under your local ACL2, we advise you to jump to Running PLTP(A) because the PLTP(A) files mentioned below require a certain amount of infrastructure (e.g., the definition of the Common Lisp symbol package named "PLTP"). But if you merely want to see how PLTP(A) is coded in ACL2 and what it can prove, browse here.


The sources for The Edinburgh Pure Lisp Theorem Prover, aka PLTP, as of 14 September, 1973, are in Listing-F and Listing-H, and have been transcribed into text form in listings-f-and-h.txt.

PLTP was written in 1972 and 1973. It was programmed in POP-2, a now dead imperative programming language, and ran on an ICL 4130 processor with 64K bytes of 2 microsecond memory shared between 8 interactive jobs controlled by teletype input from the users. File input and output was by paper tape and lineprinter.

PLTP(A) is an applicative Common Lisp implementation of the PLTP proof techniques and heuristics as of 14 September, 1973. In fact, PLTP(A) is coded in ACL2, a descendent of PLTP. PLTP(A) is not a faithful translation of the 1973 code because the known bugs and oddities of PLTP's original code have been repaired and some of the algorithms have been implemented differently while preserving a high-level equivalency to the original code as discussed further below.

PLTP(A) supports the same basic Pure Lisp as PLTP did, with primitives NIL, CAR, CDR, CONS, EQUAL and IF. (Some versions of PLTP used the symbol COND instead of IF. PLTP(A) uses IF internally but defines PLTP's 3-place COND to be IF and can optionally print IF-expressions as COND-expressions.)

PLTP(A) supports PLTP's abbreviation conventions of T (denoting (CONS NIL NIL)) and natural numbers (denoting lists of NIL). PLTP's term representation left abbreviations in place. E.g., while exploring a term the 1973 theorem prover could have encountered both the number 0 and its formal meaning, NIL. This invited programming errors, as when the 1973 EVAL transformed (CDR n) to n-1, for all natural numbers n, because we (Boyer and Moore) forgot to check that n is not 0, resulting in the transformation of (CDR 0) to the non-term -1.

In contrast, PLTP(A) translates abbreviated terms into their formal correspondents at input so that the core theorem prover only sees formal terms. This not only makes its term exploration paradigms more regular but eliminates a variety of bugs and oddities such as PLTP's failure to always treat T, 1, and (CONS NIL NIL) the same even though all three denote the same term.

PLTP(A) ``untranslates'' before printing so printed terms contain the familiar abbreviations. This can be controlled by various ``feature switches'' set by the user. See the definition of set-feature in the PLTP(A) source code.

POP-2's 8-character limitation on names produced many obscure names, e.g., GENRLT1. I have changed the names of many implementation functions, e.g., GENRLT1 is here called generalizable-subterms and GENRLIZE is now called generalize. When the new name lacks obvious correspondence to the old name (as with GENRLT1), a comment in the code gives the old name.

PLTP(A) does not attempt to reproduce exactly PLTP's English explanations of the proof steps. (The main reason for this is that it requires cluttering the code with output routines and for PLTP(A) I chose to make the generation of output as inconspicuous as possible to focus on the clarity of the term manipulation code.) But PLTP(A) takes the same steps (subject to the caveats below), describes each step in English, and prints the same intermediate formulas (again, subject to caveats below).

No longer concerned with speed and memory footprint, I've freely recoded the algorithms to return the ``same'' results, often by more elegant means. But by ``same'' I mean the proof steps taken by PLTP(A) are the same as those by the 1973 PLTP. Every intermediate formula produced by PLTP(A) logically entails the corresponding formula produced by PLTP; in fact, if one allows for variable renaming and abbreviations, corresponding formulas are usually identical. For example, where PLTP might have generated and printed

PLTP(A) might generate and print the variant (due to variable renaming):

or one of several equivalent abbreviations for that formula depending on the feature switches:



See the definition of set-feature for more explanations.

But I wrote ``usually identical'' above! There are two exceptions to this formula-by-formula identity-modulo-abbreviations: the output of PLTP(A)'s fertilization routine is a generalization of PLTP's, and the output of PLTP(A)'s induction routine is always a list-based inductive formula and never one tailored explicitly to Peano naturals. We discuss these two discrepancies, and some minor ones, below.

The important deviations from the implementation used in PLTP are as follows:

In PLTP's defense (not to mention that of Boyer and me!) I should note that the resource limitations of the 1970's ICL 4130 and the POP-2 compiler probably drove many of our implementation choices and coding style. It wasn't until 1989 and ACL2 that we adopted the much cleaner functional programming style. And that style alone does not guarantee clarity. Indeed, ACL2 today contains many less-than-elegant functional algorithms because performance still often demands code optimization despite the enormous improvement in processor speeds and memory sizes because applications have grown so much larger. Indeed, ACL2 supports functions that return a vector of values so that in one sweep of a huge formula many things can be accumulated.

The small sizes of the definitions and conjectures presented to PLTP was wonderfully freeing given today's resources!

The changes in implementation also reflect lessons learned from 45 years of coding provers together with the much more robust ACL2 programming environment I enjoy today.

Running PLTP(A)

PLTP(A) was added to ACL2's Community Books Repository in March, 2018. So if you have a recent ACL2 installation, you already have PLTP(A). Below we tell you how to run it. After that we give a brief summary of the interesting files you'll find on the books/projects/pltpa/ subdirectory of your ACL2 directory, and finally we tell you how to get ACL2 if you don't have it.

To play with PLTP(A), do

(include-book "projects/pltpa/pltpa" :dir :system)
and then select the PLTP symbol package and initialize the PLTP(A) logical world with
Then you can define PLTP functions and submit challenge theorems as with
(define (append ; define a PLTP function
	 (lambda (x y)
	   (if x (cons (car x) (append (cdr x) y)) y))))

(prove assoc-of-append ; name is irrelevant except for io; theorems are not
                       ; stored in the PLTP world

       (equal (append (append a b) c)
              (append a (append b c))))
For a complete list of available commands, e.g., to inspect PLTP's database, or undo a definition, see the comment at the top of the
PLTP(A) source file, which may be found in "books/projects/pltpa/pltpa.lisp" of your local ACL2 installation.

You can find all of the PLTP(A) files on the books/projects/pltpa/ subdirectory of your ACL2 directory.

Among the interesting files after certification of the books there you will find:

Note on how to read the .cert.out files above: Ordinarily, an ACL2 book can be certified provided the ACL2 prover can successfully prove every theorem in it. So how do we make a book that ACL2 can certify iff PLTP(A) can prove the theorems in its own regression? That involves a certain amount of infrastructure. The two .cert.out files above contain the output of ACL2's certification process. That output starts and ends with ``noise'' related to ACL2's certification infrastructure. PLTP(A)'s output (e.g., on its standard proveall) may be found between the block of text that starts with
:STANDARD Proveall by PLTP(A)
and the block that starts with
Successful :STANDARD Proveall by PLTP(A) completed on
Of course, if you have a running PLTP(A) you can see the output of the provealls by evaluating (proveall :standard) and (proveall :jacm).

If you do not already have ACL2 then you must obtain and install it in order to run PLTP(A). This also involves installing one of several available Common Lisp implementations. Follow the installation instructions under the Obtaining, Installing, and License link on the ACL2 Home Page.

The Easy Install for Unix-like Systems instructions will fetch not only the ACL2 system source code but also all of the Community Books. It is easier to fetch them all than to fetch just what you need for PLTP(A). But because PLTP(A) does not depend on any other books, you can skip the general certification instructions (e.g., Step 5 of the Easy Install for Unix-like Systems) if all you want to do is play with PLTP(A). Instead, just build your saved_acl2 runnable image and then certify the PLTP(A) books by connecting to books/projects/pltpa in your local ACL2 installation and running:

../../build/ --acl2 ../../../saved_acl2 *.lisp