--- 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.