ACL2

您可以在Wikipedia上了解到此条目的英文信息 ACL2 Thanks, Wikipedia.

ACL2（A Computational Logic for Applicative Common Lisp，应用 Common Lisp 计算逻辑）是由一个程序语言、一套一阶逻辑的可拓理论、以及一个机械化的定理证明器所组成的软件系统。ACL2从设计上支持基于归纳逻辑理论的自动推理，可应用于软件或硬件系统的验证。ACL2的编程语言与实现基于 Common Lisp。ACL2是基于BSD授权发布的开源软件。

ACL2程序语言可看作是一个函数式（无任何副作用）的 Common Lisp 变体。