# HG changeset patch
# User Oleksandr Gavenko <gavenkoa@gmail.com>
# Date 1239907278 -10800
# Node ID 613a4e9193b4e55678cc7950eaaca04852029ae6
# Parent  366b2a8bafe695a1a0a950453a9510744cb75b1d
About acl2.

diff -r 366b2a8bafe6 -r 613a4e9193b4 auto-proof.rst
--- a/auto-proof.rst	Thu Apr 16 21:27:12 2009 +0300
+++ b/auto-proof.rst	Thu Apr 16 21:41:18 2009 +0300
@@ -73,6 +73,22 @@
 
   http://formalmath.tiddlyspot.com/
 
+* ACL2.
+
+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. ACL2 is free, open source (GPL) software.
+
+  $ sudo apt-get install acl2
+
+See
+
+  http://www.cs.utexas.edu/users/moore/acl2/
+  http://en.wikipedia.org/wiki/ACL2
+
 * PVS Specification and Verification System
 
 Old (1992). Many article in 199x.