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 , at**ACL2 home page**`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
such as how to obtain and build ACL2, copyright and license material, mailing lists, connection with GitHub, and so on.**basic ``administrative'' information** may be found in The Tours. The paper**Overviews at a high level***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. at various levels are available at the ACL2-tutorial documentation topic and especially its subtopics. (There is some overlap with the present topic.)**Tutorial Introductions** include the following.**Books***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.

is introduced gently in the documentation topic, gentle-introduction-to-ACL2-programming.**Programming with ACL2** 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.**Logical basics** 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.**The theorem prover**- 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 (see ACL2-sedan) is an
and other capabilities that may be helpful for new ACL2 users.**Eclipse-based plug-in that provides a modern development environment** - A basic
is Proof Pad.**web-based interface to ACL2** - There is an ACL2 Docker container (maintained at this repo).

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