Recreation of the 1956 IPL-I version of the Logic Theorist theorem prover

Earlier this week, having come across my ArXiv paper about reanimating the Logic Theorist, David Moews (https://djm.cc/dmoews.html) wrote me about an amazing piece of work he's done:

He built an interpreter for the original IPL-I pseudocode of the original Newell and Simon Logic Theorist, straight out of the 1956 RAND report (P-868), and then got it running!

(I'll call the version that David reanimated "LT1" or "LT56", and mine "LT5" or "LT63" because mine was rewritten for IPL-V and published in 1963.)

What makes David's work especially interesting, aside from pushing the RetroAI window back 8 more years (!), is that IPL-I was NEVER ACTUALLY IMPLEMENTED! It was hand-executed by Simon's students (and supposedly his kids!) simulating the imagined IPL-I machine. This actually makes the problem much simpler. (Not at all to diminish David's accomplishment!)

In the 1956 report Newell and Simon describe the process in something close to the cognitive operators they hypothesized underlay human theorem proving. This is essentially LT1: A (somewhat) high-level specification of the Newell and Simon theory of cognitive theorem proving. But because LT1 didn't have to actually run on a real computer, it could depend upon human intelligence and flexibility to handle the complexities of actual implementation that you need to do to make a real computer actually do the whole thing end-to-end. (Or, as in David's case, a pile of Python code, which, of course, Simon and Newell didn't have in the mid 1950s!) As a result, LT1 is a bit over 400 lines whereas LT5, which is what you get when Shaw had to actually nail down the complexities of actual implementation, is nearly 3000 lines!

Anyway, huge congratulations to David; well worth a look if you care about the prehistory of AI, Lisp, or theorem proving. His repo is here: https://github.com/dmoews/logic-theorist. The readme provides a lot of intersting and important detail that I've glossed over.