ACL2_机械化的定理证明工具所组成的软件系统

ACL2

机械化的定理证明工具所组成的软件系统

ACL2（A Computational Logic for Applicative Common Lisp，应用Common Lisp计算逻辑）是由其自身的程序语言、一套可扩展的一阶逻辑理论，和一个机械化的定理证明工具所组成的软件系统。

ACL2从设计上支持基于归纳逻辑理论的自动推理，主要应用于软件或硬件系统的验证。ACL2的输入语言与实现基于Common Lisp。ACL2是基于BSD授权的开源软件。

参考资料

最新修订时间：2024-05-21 15:04

条目作者

概述

参考资料