数据词典：自动定理证明（Automatic Theorem Proving）

赵老师

自动定理证明研究如何把人类证明定理的过程变成能在计算机上自动实现符号演算的过程，就是让计算机模拟人类证明定理的方法，自动实现像人类证明定理那样的非数值符号演算过程。自动定理证明是人工智能最早进行研究并获得成功的领域之一。尽管数学定理证明过程的每一步都很严格有据，但决定采取什么样的证明步骤却依赖于经验、直觉、想象力和洞察力，需要人的智能。实际上，除了数学定理以外，还有很多非数学领域的任务，如医疗诊断、信息检索、难题求解等都可以转化成定理证明。自动定理证明的主要方法包括自动演绎法、判定法、定理证明器、人机交互定理证明等。

定理自动证明的基础是逻辑系统，传统的定理证明系统大都是建立在经典逻辑系统上的。近十几年来，不断有新的逻辑系统出现。例如，模态逻辑、模糊逻辑、时序逻辑、默认逻辑、次协调逻辑等，它们都有相应的逻辑推理规则和方法。

【出处】鲍军鹏,张选平.人工智能导论（第2版）,机械工业出版社,2021年1月.