Speaker:
J Moore

Title:
The Edinburgh Pure Lisp Theorem Prover in ACL2

Abstract:
In 1971-73, in Edinburgh, Scotland, Boyer and Moore
implemented a theorem prover for recursive functions,
called the Pure Lisp Theorem Prover (PLTP).  It was
the first prover to focus on induction and
demonstrated the power of many now-familiar proof
techniques.  PLTP eventually became NQTHM which
eventually became ACL2.  In the summer of 2017, I
recoded PLTP into ACL2.  In this talk I'll demonstrate
the ACL2 version of PLTP and show some of the
precursors of proof techniques used extensively in
ACL2 today.