ACL2 stands for ``A Computational Logic for Applicative Common Lisp.'' It was developed in collaboration with Matt Kaufmann and is an extended re-implemented version of the ``Boyer-Moore theorem prover,'' Nqthm, developed in collaboration with Bob Boyer.
The theorem prover interacts with the user (who submits definitions, conjectures and advice) and with a collection of ``books'' derived from previously proved theorems.