ACL2（A Computational Logic for Applicative Common Lisp，套用Common Lisp計算邏輯）是由其自身的程式語言、一套可擴展的一階邏輯理論，和一個機械化的定理證明工具所組成的軟體系統。 基本介紹 中文名：ACL2外文名：A Computational Logic for Applicative Common Lisp別名：套用Common Lisp計算邏輯基於：BSD授權的開源軟體 ACL2從設計上支持基於歸納邏輯理論的自動推理，主要套用於軟體或硬體系統的驗證。ACL2的輸入語言與實現基於Common Lisp。ACL2是基於BSD授權的開源軟體。
