ACL2

ACL2（A Computational Logic for Applicative Common Lisp，應用式 Common Lisp 計算邏輯）係由一個程序語言、一套一階邏輯嘅可拓理論同埋一個機械化嘅定理證明器所組成嘅軟件系統。ACL2 由設計上支持基於歸納邏輯理論嘅自動推理，可應用喺軟件或者硬件系統嘅形式化驗證。 ACL2 嘅編程語言同佢嘅實現基於 Common Lisp。ACL2 係基於BSD授權發布嘅開源軟件。