(资料图)

1、 定理机器证明是用计算机自动地进行推理和证明数学定理。

2、又称为自动定理证明(ATP)。

3、让机器去证明数学定理的想法，在17世纪G.W.Leibniz 创立数理逻辑时就产生了，但这一想法的真正实现，是在20世纪40年代计算机诞生以后。