		Search-engine friendly clone of the ACL2 documentation.

ACL2

Start-here

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 in The 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 topic.)
Books include the following.

Computer-Aided Reasoning: An Approach provides a detailed introduction to ACL2 and contains many exercises.
Computer-Aided Reasoning: ACL2 Case Studies describes some relatively early applications of ACL2, including scripts as well as answers to the exercises.

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 online manual.
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 tool.
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)?”.
Here are some resources for trying out ACL2 without directly installing it yourself.

The 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 Proof Pad.
There is an ACL2 Docker container (maintained at this repo).

Subtopics

Gentle-introduction-to-ACL2-programming: A Gentle Introduction to ACL2 Programming
ACL2-tutorial: Tutorial introduction to ACL2
About-ACL2: General information About ACL2