以計算機證明數學定理為例，從公理係統的公理出發，用枚舉法證明。如果推理一步，

可以枚舉出N個定理。如果從公理加上這N個定理中的任何一個定理再往前推理一步，至少可以枚舉出M個定理。那麽兩步推理就會得到N＊M個定理。

 

這樣隻要幾步推理，計算機就達到極限了。如果某個定理至少要X步推理，X很可能超出了計算機的極限。所以計算機證明數學定理非常困難。速度越快，內存越多，計算機證明數學定理的能力就越強。

所有跟帖： 

• 多說一句：公理係統的定理證明隻是半可計算的。 -加州老李- ♀ (346 bytes) () 10/29/2010 postreply 14:19:44

• Thanks! -xinliji- ♀ (0 bytes) () 10/30/2010 postreply 11:05:11