PLTP(R): Resurrecting POP-2 and PLTP

Robert S. Boyer
Grant O. Passmore
J Strother Moore
August, 2017 As noted in the background discussions above, the original goal of this effort was to run the POP-2 code for the 14 September, 1973, core of the prover on a modern (2017) processor. Also as noted, this effort was ultimately unsuccessful because the only POP-2 implementation we could find was fragile, undocumented, and suffered memory limitations even more severe than those we dealt with in Edinburgh in 1973. We had to make extensive modifications to the original source code to get it through the compiler without compile-time errors and aborts and even then it exhibited runtime errors during some proof attempts. We call the modified system PLTP(R). It successfully completes 82 of 107 test theorems found in Moore's dissertation, the 1975 JACM paper, and various listings. We lost interest in PLTP(R) because even if we'd managed to get error-free proof runs, we would not be running the 1973 source code, which was the whole point. But in the interest of the historical record, the product of this effort is recorded here.