李娜：机器证明的逻辑推定

逻辑定理的机器证明是人工智能领域人们最早从事研究的课题。《机器证明的逻辑推定》从逻辑定理的人工证明和机器证明两方面来展现逻辑定理证明的艺术，而机器证明又从定理的自动证明和计算机辅助证明两个方面来展现。本书首先用作者构造的命题演算系统 FPC 和狭谓词演算系统 FQC 完成常用逻辑定理的人工证明(一种自然推理证明)。其次，用逻辑定理的机器证明工具 TPG(Tree Proof Generator)实现逻辑定理的自动证明(一 种树证明)。最后，用交互式定理机器证明工具 Fitch 实现了逻辑定理的计算机证明(一种自然推理证明)。

本书可作为哲学、逻辑学、数学、语言学等相关专业学生学习逻辑学的参考书，也可为人工智能相关研究者提供参考。