ACL2

来自开放百科 - 灰狐
(版本间的差异)
跳转到: 导航, 搜索
(链接)
第1行: 第1行:
 
{{SeeWikipedia}}
 
{{SeeWikipedia}}
  
 +
ACL2
 +
 +
==简介==
 
ACL2(A Computational Logic for Applicative [[Common Lisp]],应用 Common Lisp 计算逻辑)是由一个程序语言、一套一阶逻辑的可拓理论、以及一个机械化的定理证明器所组成的软件系统。ACL2从设计上支持基于归纳逻辑理论的自动推理,可应用于软件或硬件系统的验证。ACL2的编程语言与实现基于 Common Lisp。ACL2是基于BSD授权发布的开源软件。
 
ACL2(A Computational Logic for Applicative [[Common Lisp]],应用 Common Lisp 计算逻辑)是由一个程序语言、一套一阶逻辑的可拓理论、以及一个机械化的定理证明器所组成的软件系统。ACL2从设计上支持基于归纳逻辑理论的自动推理,可应用于软件或硬件系统的验证。ACL2的编程语言与实现基于 Common Lisp。ACL2是基于BSD授权发布的开源软件。
  
ACL2程序语言可看作是一个函数式(无任何副作用)的 Common Lisp 变体。
+
ACL2 程序语言可看作是一个函数式(无任何副作用)的 Common Lisp 变体。
 +
 
 +
==[[Proof assistant|形式化验证]]==
 +
*[https://www.cs.utexas.edu/users/moore/acl2/v8-4/combined-manual/index.html?topic=ACL2____HARDWARE-VERIFICATION Hardware-verification]
 +
*[https://www.cs.utexas.edu/users/moore/acl2/v8-4/combined-manual/index.html?topic=ACL2____SOFTWARE-VERIFICATION Software-verification]
 +
*[https://www.cs.utexas.edu/users/moore/acl2/v8-4/combined-manual/index.html?topic=ACL2____PROOF-AUTOMATION Proof-automation]
 +
 
 +
==功能==
 +
 
 +
==指南==
 +
 
 +
==项目==
 +
 
 +
==图集==
  
 
==链接==
 
==链接==
 
*[http://www.cs.utexas.edu/users/moore/acl2/ ACL2官网]
 
*[http://www.cs.utexas.edu/users/moore/acl2/ ACL2官网]
 +
*[https://github.com/acl2/acl2/ ACL2 @ GitHub]
 
*[http://docs.huihoo.com/lisp/acl2 ACL2文档]
 
*[http://docs.huihoo.com/lisp/acl2 ACL2文档]
  
 
[[category:lisp]]
 
[[category:lisp]]
 +
[[category:proof assistant]]
 
[[category:programming language]]
 
[[category:programming language]]

2021年12月22日 (三) 09:53的版本

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

ACL2

目录

简介

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

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

形式化验证

功能

指南

项目

图集

链接

分享您的观点
个人工具
名字空间

变换
操作
导航
工具箱