Introductory information about ACL2
This documentation topic provides a starting point for those
who are new to ACL2 or want to learn more about it. It accommodates different
goals (ranging from mild curiosity about ACL2 to the desire to become an
expert user) and different learning styles. A quick scan should help you find
a place to start that suits you.
- The ACL2 home page, at
http://www.cs.utexas.edu/users/moore/acl2/, provides links that can
take you to good places to start learning about ACL2.
- See about-ACL2 for basic ``administrative''
information such as how to obtain and build ACL2, copyright and
license material, mailing lists, connection with GitHub, and so on.
- Overviews at a high level may be found
Tours. The paper Industrial
Proofs with ACL2 was written in the 1990s but is still useful for
providing a brief overview of what can be done with ACL2.
- Tutorial Introductions at various
levels are available at the ACL2-tutorial documentation topic and
especially its subtopics. (There is some overlap with the present
- Books include the following.
- There are many projects that use ACL2.
- See interesting-applications for an overview of some projects that
have used ACL2.
- A publications
page has links to many books and papers. You can also follow links
starting at the ACL2
Workshops page to see programs, talks, and papers presented at ACL2
Workshops (25 and counting as of 2022).
- The Community
Books is a repository of many projects, processed virtually continuously
by virtue of constituting the ACL2 regression suite. Many of those projects
are descried in the ACL2+books
- Programming with ACL2 is introduced
gently in the documentation topic, gentle-introduction-to-ACL2-programming.
- Logical basics are presented in the
recursion-and-induction documentation topic, for teaching yourself how
to prove theorems about recursively defined functions using mathematical
induction. There are lots of exercises. Some may find this a good way to get
into ACL2, by understanding its proof system before attempting to use the
- The theorem prover is something
perhaps best learned after studying the logical basics above, or at least
giving them a quick glance. Then you can just dive in or you can first study
how to use it.
- See the-method for concise guidance on the key technique for using
the ACL2 prover effectively.
- See introduction-to-the-theorem-prover for a detailed discussion of
how to be an effective user of the ACL2 theorem prover, including a focus on
its primary proof technique, rewriting.
- The paper “How
to Prove Theorems Formally guides the reader towards effective use of
ACL2, with exercises included. Quoting the abstract: “The real purpose
of this paper is to answer the question how does one construct and manage
large mechanically checked proofs (in ACL2)?”.
- The ACL2 Sedan (see ACL2-sedan) is an Eclipse-based plug-in that provides
a modern development environment and other capabilities that may
be helpful for new ACL2 users.
- A basic web-based interface to ACL2 is
- A Gentle Introduction to ACL2 Programming
- Tutorial introduction to ACL2
- General information About ACL2