自動定理證明

自動定理證明，目的是為使用電子電腦程式來進行數學定理的證明。

自動定理證明 (ATP)

目前是自動推理(AR)體系中發展最好的部分，它的目的是為使用電子電腦程式來進行數學定理的證明。對於不同的數學邏輯，它能夠推論出一個定理是正確的，還是不可證明的，或者錯誤的。