Tags: Programming Language.

ACL2 (A Computational Logic for Applicative Common Lisp) is a software system consisting of a programming language an extensible theory in a first-order logic and a mechanical theorem prover. ACL2 is designed to support automated reasoning in inductive logical theories mostly for the purpose of software and hardware verification. The input language and implementation of ACL2 are built on Common Lisp.

Loading...

This page contains content from the copyrighted Wikipedia article "ACL2"; that content is used under the GNU Free Documentation License (GFDL). You may redistribute it, verbatim or modified, providing that you comply with the terms of the GFDL.