ACL2

ACL2（A Computational Logic for Applicative Common Lisp，應用Common Lisp計算邏輯）是由其自身的程序語言、一套可擴展的一階邏輯理論，和一個機械化的定理證明工具所組成的軟體系統。