ACL2
维基百科,自由的 encyclopedia
ACL2(A Computational Logic for Applicative Common Lisp,应用式 Common Lisp 计算逻辑)是由一个程序语言、一套一阶逻辑的可拓理论、以及一个机械化的定理证明器所组成的软件系统。ACL2 从设计上支持基于归纳逻辑理论的自动推理,可应用于软件或硬件系统的形式化验证。ACL2 的编程语言及其实现基于 Common Lisp。ACL2 是基于BSD授权发布的开源软件。
Quick Facts 编程范型, 设计者 ...
![]() | |
编程范型 | 函数式编程、元编程 |
---|---|
设计者 | 罗伯特·斯蒂芬·博伊尔 斯特罗瑟·摩尔 马特·考夫曼 |
实作者 | 马特·考夫曼 斯特罗瑟·摩尔 |
发行时间 | 1990年(内部发布) 1996年(公开发布) |
型态系统 | 动态类型 |
操作系统 | 跨平台 |
许可证 | BSD License |
网站 | ACL2 |
启发语言 | |
Common Lisp、NQTHM |
Close