欢迎大家赞助一杯啤酒🍺 我们准备了下酒菜：Formal mathematics/Isabelle/ML, Formal verification/Coq/Agda, C++/Erlang/Lisp
ACL2
来自开放百科 - 灰狐
（版本间的差异）
(以“{{SeeWikipedia}} ACL2（A Computational Logic for Applicative Common Lisp，应用 Common Lisp 计算逻辑）是由一个程序语言、一套一阶逻辑的...”为内容创建页面) |
小 (→链接) |
||
| 第7行： | 第7行： | ||
==链接== | ==链接== | ||
*[http://www.cs.utexas.edu/users/moore/acl2/ ACL2官网] | *[http://www.cs.utexas.edu/users/moore/acl2/ ACL2官网] | ||
| − | *[http://docs.huihoo.com/acl2 ACL2文档] | + | *[http://docs.huihoo.com/lisp/acl2 ACL2文档] |
[[category:lisp]] | [[category:lisp]] | ||
[[category:programming language]] | [[category:programming language]] | ||
2015年10月17日 (六) 00:13的版本
|
您可以在Wikipedia上了解到此条目的英文信息 ACL2 Thanks, Wikipedia. |
ACL2（A Computational Logic for Applicative Common Lisp，应用 Common Lisp 计算逻辑）是由一个程序语言、一套一阶逻辑的可拓理论、以及一个机械化的定理证明器所组成的软件系统。ACL2从设计上支持基于归纳逻辑理论的自动推理，可应用于软件或硬件系统的验证。ACL2的编程语言与实现基于 Common Lisp。ACL2是基于BSD授权发布的开源软件。
ACL2程序语言可看作是一个函数式（无任何副作用）的 Common Lisp 变体。
链接
分享您的观点
