自動化定理證明（Automated theorem proving，簡稱ATP）目前是自動推理（Automated reasoning，簡稱AR）體系中發展最好的部分，它的目的是為使用電子電腦程式來進行數學定理的證明。對於不同的公理系統，它能夠推論出一個定理在此系統下是正確的，還是不可證明的，或者錯誤的。 此條目沒有列出任何參考或來源。 (2024年5月16日) agda2中的一個證明例子 參考 電腦協助證明 這是一篇關於數學的小作品。您可以透過編輯或修訂擴充其內容。閱論編 Wikiwand - on Seamless Wikipedia browsing. On steroids.
agda2中的一個證明例子
