概念Automated Theorem Proving / ATP
自动定理证明
自动定理证明（Automated Theorem Proving，ATP）是计算机科学与数学逻辑的交叉研究领域，旨在通过计算机程序自动推导并验证数学命题或逻辑公式的正确性。其核心方法包括归结原理、模型检验、交互式证明辅助等，代表系统有Coq、Lean、Isabelle等。广泛应用于形式化数学、程序正确性验证及硬件逻辑验证等领域。
时间轴 (近 90 天)
10月4日
自动定理证明器（ATP）如Vampire和E-prover无需人工干预，适合处理一阶逻辑范围内的问题
待验证50%
8月20日
Allen Newell和Herbert Simon在CMU开发了最早的AI程序之一'逻辑理论家'（Logic Theorist），AI研究可追溯到1956年
待验证50%