GitHub - dmoews/logic-theorist: Recreation of the 1956 IPL-I version of the Logic Theorist theorem prover.

The 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) ( q -> ( p \/ q ) ) (*1.3) ( ( p \/ q ) -> ( q \/ p ) ) (*1.4) ( ( p \/ ( q \/ r ) ) -> ( q \/ ( p \/ r ) ) ) (*1.5) and ( ( q -> r ) -> ( ( p \/ q ) -> ( p \/ r ) ) ) (*1.6.)

The rules of inference are detachment (*1.11), where q is inferred from p and ( p -> q ), and substitution of expressions into the propositional variables of a known axiom or theorem. (Although substitution is not stated as an explicit deduction rule in Principia Mathematica, it is used extensively and admitted to be admissible at the beginning of *2.) Apart from substitution and detachment, the Logic Theory Machine also uses the proof method of chaining, where ( p -> r ) is inferred from ( p -> q ) and ( q -> r ). This can be justified by the theorems *2.05 or *2.06 in Principia Mathematica. About the code The Python files meant to be run directly here are logic.py, run_logic.py, and analyze_output.py. They will all print basic usage information when invoked with the --help option. logic.py is the interpreter for the IPL-I abstract machine. analyze_output.py is intended to extract the proof found, if any, from the output printed by logic.py, since there was no provision to do that in the provided IPL-I source code. It's best to use it with the --info option of logic.py. run_logic.py is intended to imitate [1] by running the program successively on each of the theorems in *2 of Principia Mathematica, allowing it to use, in the proof of each theorem, all axioms and all previous theorems from *2, whether it managed to prove them or not.

File list

README.md — this file IPL-I source code:

logic-routines.txt — IPL-I source code for the Logic Theory Machine, revised so as to be runnable orig-logic-routines.txt — Original IPL-I source code for the Logic Theory Machine as printed in [7]; labels, opcodes and operands only transcription.txt — transcription of all source code as printed in [7], including comments

Principia Mathematica:

pm-axioms.txt — The five propositional logic axioms from *1 in Principia Mathematica pm-theorems.txt — The theorems from *2 in Principia Mathematica

IPL-I interpreter:

analyze_output.py — Program to extract and check the proof found by the interpreter grammar.py — Module with CFG routines logic.py — Interpreter for the IPL-I abstract machine run_logic.py — Driver program simple_parser.py — Module with CFG parser utils.py — Module with grammar and substitution utility routines

Testing:

test.sh, test.py — Testing framework analyze_output.test, analyze_output.test-input, analyze_output.usage — tests for analyze_output.py logic.test, test-source.txt, test-source-2.txt, test-source-3.txt, test-theorems-1.txt, test-theorems-2.txt, test-theorems-3.txt, logic.usage — tests for logic.py run_logic.test, say-hi.py, run_logic.usage — tests for run_logic.py verify.py — check consistency of the source code in orig-logic-routines.txt with that in transcription.txt

References There is a good deal of additional information about the Logic Theory Machine/Logic Theorist in the CMU Digital Collection archives, which contain special collections on Newell and Simon. See the URL https://digitalcollections.library.cmu.edu/, and in particular https://digitalcollections.library.cmu.edu/cmu-collection/allen-newell and https://digitalcollections.library.cmu.edu/cmu-collection/herbert-simon.

[1]: Empirical Explorations of the Logic Theory Machine: a Case Study in Heuristic, A. Newell, J. C. Shaw, H. A. Simon, IRE-AIEE-ACM '57 (Western): Papers presented at the February 26-28, 1957, Western joint computer conference: Techniques for reliability, Feb. 1957, pp. 218-230, DOI: 10.1145/1455567.1455605. [2]: Introduction to the First Edition in: Information Processing Language-V Manual, second ed., Allen Newell et al., RAND Corporation, pub. Englewood Cliffs, NJ : Prentice-Hall, Inc., 1964, https://archive.org/details/bitsavers_randiplInfanguageVSecondEdition1964_15001417. [3] Chapter 13, Models of My Life, Herbert A. Simon, Cambridge, Mass., etc.: MIT Press, 1996 (first pub. 1991, Basic Books.) [4] Programming the Logic Theory Machine, A. Newell, J. C. Shaw, IRE-AIEE-ACM '57 (Western): Papers presented at the February 26-28, 1957, Western joint computer conference: Techniques for reliability, Feb. 1957, pp. 230-240, DOI: 10.1145/1455567.1455606. [5] Introduction in: The Logic Theory Machine: A Model Heuristic Program, Einar Stefferud, RAND Research Memorandum RM-3731-CC, June 1963, https://www.rand.org/pubs/research_memoranda/RM3731.html. [6] The Logic Theory Machine--A Complex Information Processing System, A. Newell, H. Simon, IRE Transactions on Information Theory 2, #3 (September 1956), pp.

61-79, DOI: 10.1109/TIT.1956.1056797. [7] The Logic Theory Machine: A Complex Information Processing System, Allen Newell, Herbert A. Simon, RAND paper P-868, July 12, 1956, Revised, https://archive.org/details/bitsavers_randiplP86ineJul56_3534001. (This is extremely similar to [6].) [8] *1 and *2, Principia Mathematica, A. N. Whitehead and B. Russell, Volume I, Cambridge: Cambridge University Press, 1910. Available on HathiTrust; see https://hdl.handle.net/2027/miun.aat3201.0001.001?urlappend=%3Bseq=117.