自动定理证明

自动定理证明（简称ATP）是自动推理(automated reasoning）以及数理逻辑（利用计算机程序进行数学定理证明）的分支。以数学证明为基础的自动推理曾经是计算机科学发展的主要驱动力。