PLTP(O): PLTP in OCAML

Grant O. Passmore
August, 2017 Working from Moore's dissertation and the 1975 JACM paper, I produced a version of PLTP in OCaml. We call this PLTP(O) here and stress that unlike PLTP(R) and PLTP(A), this system was not based on the original source code but from descriptions of it. Despite the care taken by Boyer and Moore in writing those descriptions, I inevitably had to make some judgement calls about the details of some of the techniques. PLTP(O) instructions, OCAML source code, tests, and proofs are available at PLTP in OCAML