dmoews/logic-theorist

来源：https://github.com/dmoews/logic-theorist
本代码的目标是实现首个公开版本的逻辑理论机（Logic Theory Machine，亦称 Logic Theorist）。

逻辑理论机

逻辑理论机是由 Allen Newell、J. C. Shaw 和 Herbert A. Simon 在启发式问题解决方法研究过程中编写的程序。它旨在利用《数学原理》[1]中的逻辑系统证明命题逻辑定理。Newell 和 Simon 于 1955 年末左右开始编写该程序。他们最初通过手工模拟程序，一度借助 Simon 的妻子、孩子以及一些研究生协助进行。[3]程序最初用一种名为 IPL-I 的伪代码编写，但该伪代码从未实际实现。[2][3]首个在计算机上运行的版本采用 IPL-II 编写，并在 JOHNNIAC 计算机上运行，于 1956 年 8 月产生第一个证明。[1][2][3][4]随后由 Fred Tonge 转换为 IPL-V，并由 Einar Stefferud 进一步开发。[5]

逻辑理论机首个公开版本

一个早期版本的逻辑理论机源代码于 1956 年发表在文献 [6] 和 [7] 中；该代码采用 IPL-I 编写，这是一种面向抽象机器的类汇编语言。两份参考文献中的代码几乎完全相同。遗憾的是，代码中存在一些拼写错误和问题，其印刷形式无法直接运行。我已尝试按需修复这些问题，具体说明见源代码文件。

逻辑系统

《数学原理》[8] 中的命题逻辑系统通过一元否定（~）和二元或（\/）从命题变量构建公式。蕴涵（->）定义为 ( p -> q ) 等于 ( ~ p \/ q )，这两个表达式视为可互换（*1.01）。五个公理如下：

• ( ( p \/ p ) -> p ) (*1.2)
• ( q -> ( p \/ q ) ) (*1.3)
• ( ( p \/ q ) -> ( q \/ p ) ) (*1.4)
• ( ( p \/ ( q \/ r ) ) -> ( q \/ ( p \/ r ) ) ) (*1.5)
• ( ( q -> r ) -> ( ( p \/ q ) -> ( p \/ r ) ) ) (*1.6)
  推理规则包括分离规则（*1.11），即从 p 和 ( p -> q ) 推断出 q；以及将表达式代入已知公理或定理的命题变量中（尽管在《数学原理》中，代入并未被明确列为演绎规则，但在 *2 开头被广泛使用并承认是可接受的）。除代入和分离外，逻辑理论机还使用了链式证明方法，即从 ( p -> q ) 和 ( q -> r ) 推断出 ( p -> r )。这可由《数学原理》中的定理 *2.05 或 *2.06 证明。

关于代码

此处可直接运行的 Python 文件包括 logic.py、run_logic.py 和 analyze_output.py。使用 --help 选项调用时，它们将打印基本用法信息。
logic.py 是 IPL-I 抽象机器的解释器。
analyze_output.py 旨在从 logic.py 打印的输出中提取找到的证明（如果有的话），因为提供的 IPL-I 源代码中没有相关的打印机制。建议与 logic.py 的 --info 选项配合使用。
run_logic.py 旨在模仿文献 [1]，在《数学原理》*2 中的每个定理上依次运行程序，允许在证明每个定理时使用所有公理以及 *2 中之前的全部定理（无论是否成功证明它们）。

文件列表

• README.md — 本文件
• IPL-I 源代码：
  • logic-routines.txt — 逻辑理论机的 IPL-I 源代码，已修订为可运行版本
  • orig-logic-routines.txt — 文献 [7] 中印刷的原始 IPL-I 源代码，仅包含标签、操作码和操作数
  • transcription.txt — 文献 [7] 中所有源代码的转录，包括注释
• 《数学原理》：
  • pm-axioms.txt — 《数学原理》*1 中的五个命题逻辑公理
  • pm-theorems.txt — 《数学原理》*2 中的定理
• IPL-I 解释器：
  • analyze_output.py — 提取并验证解释器所找到的证明的程序
  • grammar.py — 包含 CFG 例程的模块
  • logic.py — IPL-I 抽象机器的解释器
  • run_logic.py — 驱动程序
  • simple_parser.py — 包含 CFG 解析器的模块
  • utils.py — 包含语法和代入工具例程的模块
• 测试：
  • test.sh, test.py — 测试框架
  • analyze_output.test, analyze_output.test-input, analyze_output.usage — 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 — logic.py 的测试
  • run_logic.test, say-hi.py, run_logic.usage — run_logic.py 的测试
  • verify.py — 验证 orig-logic-routines.txt 中的源代码与 transcription.txt 的一致性

参考文献

关于逻辑理论机/逻辑理论家的更多信息，请参见 CMU 数字馆藏档案，其中包含 Newell 和 Simon 的专题收藏。见 URL ，特别是 和 。
[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 (https://dx.doi.org/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, .
[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 (https://dx.doi.org/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, .
[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 (https://dx.doi.org/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, . (与 [6] 极为相似.)
[8] *1 and *2, Principia Mathematica, A. N. Whitehead and B. Russell, Volume I, Cambridge: Cambridge University Press, 1910. 可在 HathiTrust 获取；参见 .