自動化定理證明

维基百科,自由的百科全书
(重定向自自动定理证明
agda2中的一个证明例子

自動化定理證明Automated theorem proving,簡稱ATP)目前是自动推理(Automated reasoning,簡稱AR)体系中发展最好的部分,它的目的是为使用电子计算机程序来进行数学定理证明。对于不同的公理系统,它能够推论出一个定理在此系统下是正确的,还是不可证明的,或者错误的。

參考[编辑]