自動化定理證明

自動化定理證明Automated theorem proving,簡稱ATP)目前是自動推理(Automated reasoning,簡稱AR)體系中發展最好的部分,它的目的是為使用電子電腦程式來進行數學定理證明。對於不同的公理系統,它能夠推論出一個定理在此系統下是正確的,還是不可證明的,或者錯誤的。

agda2中的一個證明例子

參考