Python-based IPL-I interpreter resurrects the 1956 Newell-Shaw-Simon Logic Theorist, running the original RAND report pseudocode to prove Principia Mathematica theorems.
Key Takeaways
The original IPL-I source (RAND P-868, 1956) was never implemented on hardware; this repo is the first working interpreter for that pseudocode.
logic.py implements the IPL-I abstract machine; run_logic.py drives it through all theorems in *2 of Principia Mathematica sequentially, chaining prior results.
The prover uses substitution, detachment (1.11), and chaining derived from 2.05/*2.06 – the exact inference rules Newell and Simon specified.
Printed source had typos; dmoews corrected and documented all repairs, preserving the original in orig-logic-routines.txt alongside the runnable logic-routines.txt.
analyze_output.py is needed to extract proofs post-run because the 1956 IPL-I code itself had no output mechanism for proof traces.
Hacker News Comment Review
The sole commenter is the author of a related ArXiv paper on reanimating the Logic Theorist, confirming dmoews contacted them after independently building and running the IPL-I interpreter – two parallel revival efforts converging.
Notable Comments
@abrax3141: confirms dmoews built an IPL-I interpreter directly from the 1956 RAND P-868 report and got it running, calling it “LT1”.
