BTW, squashed the bug, and now it's producing complete and correct results!

https://github.com/jeffshrager/IPL-V/blob/master/major_resul...

(Well, there's a minor printout issue, but the proofs are working correctly!)

I have successfully reanimated Simon, Newell, and Shaw’s Logic Theorist, the world's first AI[note], on an IPL-V emulator written in Lisp! This dribble shows it proving 11 complete theorems from the original Principia (or, at least from Simon and Newell's original inputs, which claim to have been from the Principia. I haven't checked.)

(It does break at the end, and I haven't started to track that down -- it may actually be my own runaway limiters that tripped it.)

[note] Or at worst the second -- depending on whether you count Arthur Samuel's first checkers player. But certainly LT is the first cognitive model, and first explicitly symbol processing AI.

The header URL got trashed use: https://github.com/jeffshrager/IPL-V/