GoKawiilThe aim of this code is to implement the first published version of the Logic Theory Machine (also called the Logic Theorist.)
The Logic Theory Machine
The Logic Theory Machine was a program written by Allen Newell, J. C. Shaw, and Herbert A. Simon as part of their research into heuristic methods of problem-solving. It was intended to prove theorems in propositional logic, using the logical system for this in Principia Mathematica. [1] Newell and Simon began writing the program around the end of 1955. They initially simulated the program by hand, at one point using Simon's wife, children and some graduate students to help them. [3] It was at first written in a pseudocode called IPL-I, which was never implemented. [2], [3] The first version that was run on a computer was written in IPL-II and ran on the JOHNNIAC, producing its first proof in August 1956. [1], [2], [3], [4] It was later converted into IPL-V by Fred Tonge, and further developed by Einar Stefferud. [5]
The first published version of the Logic Theory Machine
The source code for an early version of the Logic Theory Machine was published in 1956 in [6] and [7]; it was written in IPL-I, an assembler-like language for an abstract machine. The code is almost identical in both references. The code unfortunately has some typos and problems and is not immediately runnable in its printed form. I have tried to repair it as necessary, as explained in the source code files.
The logical system
The propositional logic system in Principia Mathematica [8] builds formulae up from propositional variables by means of unary negation ( ~ ) and binary or ( \/ ). Implication ( -> ) is defined by letting ( p -> q ) equal ( ~ p \/ q ) , and these two expressions are treated as interchangeable (*1.01.) The five axioms are:
( ( p \/ p ) -> p ) (*1.2)
(*1.2) ( q -> ( p \/ q ) ) (*1.3)
(*1.3) ( ( p \/ q ) -> ( q \/ p ) ) (*1.4)
... continue reading