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