Pages Written Especially for the Tours

The ACL2 Home Page is generated from ACL2's online documentation strings. (How else could we achieve the total integration of ACL2's online documentation with the home page?) This page is just an artifact of the structure of our documentation strings: each string must belong to a ``major section'' of the documentation database. This page is not structured to be used by a person browsing via the Web. It contains, in an arbitrary order, the pages written specifically for the Web user.

Furthermore, browsing the pages below as text, in particular using the ACL2 :DOC command, is often unsatisfying because because of the lack of support for displaying gif files or for going ``back'' to a node just visited. If you wish to look at the pages below, we strongly recommend that you do so via a HTML-based Web browser. Indeed, you should simply visit ACL2's Home Page and take one of the Tours.

Generally, the topics listed above will not be of use to the ACL2 user.

- A Tiny Warning Sign
- A Tiny Warning Sign
- About the Prompt
- About the Prompt
- ACL2 Symbols
- ACL2 Symbols
- Common Lisp
- Common Lisp
- About Types
- About Types
- The Event Summary
- The Event Summary
- An Example of ACL2 in Use
- An Example of ACL2 in Use
- The Tours
- The Tours
- Corroborating Models
- Corroborating Models
- The Proof of the Associativity of App
- The Proof of the Associativity of App
- Guards in ACL2
- Guards
- Numbers in ACL2
- Numbers in ACL2
- About the Admission of Recursive Definitions
- About the Admission of Recursive Definitions
- Free Variables in Top-Level Input
- Free Variables in Top-Level Input
- Common Lisp as a Modeling Language
- Common Lisp as a Modeling Language
- ACL2 as an Interactive Theorem Prover (cont)
- ACL2 as an Interactive Theorem Prover (cont)
- A Flying Tour of ACL2
- A Flying Tour of ACL2
- Analyzing Common Lisp Models
- Analyzing Common Lisp Models
- A Walking Tour of ACL2
- A Walking Tour of ACL2
- The Theorem that App is Associative
- The Theorem that App is Associative
- The End of the Walking Tour
- The End of the Walking Tour
- Proving Theorems about Models
- Proving Theorems about Models
- Functions for Manipulating these Objects
- Functions for Manipulating these Objects
- About the ACL2 Home Page
- About the ACL2 Home Page
- ACL2 Conses or Ordered Pairs
- ACL2 Conses or Ordered Pairs
- The Associativity of App
- The Associativity of App
- Models of Computer Hardware and Software
- Models of Computer Hardware and Software
- How To Find Out about ACL2 Functions (cont)
- How To Find Out about ACL2 Functions (cont)
- A Sketch of How the Rewriter Works
- A Sketch of How the Rewriter Works
- ACL2 System Architecture
- ACL2 System Architecture
- Running Models
- Running Models
- ACL2 is an Untyped Language
- ACL2 is an Untyped Language
- How To Find Out about ACL2 Functions
- How To Find Out about ACL2 Functions
- How Long Does It Take to Become an Effective User(Q)
- How Long Does It Take to Become an Effective User?
- The Admission of App
- The Admission of App
- Guiding the ACL2 Theorem Prover
- Guiding the ACL2 Theorem Prover
- What Is ACL2(Q)
- What Is ACL2?
- Conversion
- Conversion to Uppercase
- An Example Common Lisp Function Definition
- An Example Common Lisp Function Definition
- ACL2 Characters
- ACL2 Characters
- You Must Think about the Use of a Formula as a Rule
- You Must Think about the Use of a Formula as a Rule
- The WARNING about the Trivial Consequence
- The WARNING about the Trivial Consequence
- Guessing the Type of a Newly Admitted Function
- Guessing the Type of a Newly Admitted Function
- ACL2 Strings
- ACL2 Strings
- What is a Mathematical Logic(Q)
- What is a Mathematical Logic?
- Revisiting the Admission of App
- Revisiting the Admission of App
- What is a Mechanical Theorem Prover(Q)
- What is a Mechanical Theorem Prover?
- About Models
- About Models
- What is Required of the User(Q)
- What is Required of the User?
- Hey Wait! Is ACL2 Typed or Untyped(Q)
- Hey Wait! Is ACL2 Typed or Untyped?
- The Falling Body Model
- The Falling Body Model
- Rewrite Rules are Generated from DEFTHM Events
- Rewrite Rules are Generated from DEFTHM Events
- A Typical State
- A Typical State
- The Time Taken to do the Associativity of App Proof
- The Time Taken to do the Associativity of App Proof
- The Simplification of the Induction Conclusion (Step 1)
- The Simplification of the Induction Conclusion (Step 1)
- The Rules used in the Associativity of App Proof
- The Rules used in the Associativity of App Proof
- Subsumption of Induction Candidates in App Example
- Subsumption of Induction Candidates in App Example
- Other Requirements
- Other Requirements
- Models in Engineering
- Models in Engineering
- Symbolic Execution of Models
- Symbolic Execution of Models
- Suggested Inductions in the Associativity of App Example
- Suggested Inductions in the Associativity of App Example
- Overview of the Proof of a Trivial Consequence
- Overview of the Proof of a Trivial Consequence
- Evaluating App on Sample Input
- Evaluating App on Sample Input
- The Induction Step in the App Example
- The Induction Step in the App Example
- Modeling in ACL2
- Modeling in ACL2
- The Simplification of the Induction Conclusion (Step 9)
- The Simplification of the Induction Conclusion (Step 9)
- The Induction Scheme Selected for the App Example
- The Induction Scheme Selected for the App Example
- The First Application of the Associativity Rule
- The First Application of the Associativity Rule
- Overview of the Expansion of ENDP in the Induction Step
- Overview of the Expansion of ENDP in the Induction Step
- Flawed Induction Candidates in App Example
- Flawed Induction Candidates in App Example
- ACL2 as an Interactive Theorem Prover
- ACL2 as an Interactive Theorem Prover
- Using the Associativity of App to Prove a Trivial Consequence
- Using the Associativity of App to Prove a Trivial Consequence
- The Simplification of the Induction Conclusion (Step 8)
- The Simplification of the Induction Conclusion (Step 8)
- The Instantiation of the Induction Scheme
- The Instantiation of the Induction Scheme
- The Final Simplification in the Base Case (Step 0)
- The Final Simplification in the Base Case (Step 0)
- Overview of the Simplification of the Induction Step to T
- Overview of the Simplification of the Induction Step to T
- Overview of the Simplification of the Induction Conclusion
- Overview of the Simplification of the Induction Conclusion
- On the Naming of Subgoals
- On the Naming of Subgoals
- Nontautological Subgoals
- Prover output omits some details
- What is a Mechanical Theorem Prover(Q) (cont)
- What is a Mechanical Theorem Prover? (cont)
- The Simplification of the Induction Conclusion (Step 12)
- The Simplification of the Induction Conclusion (Step 12)
- The Simplification of the Induction Conclusion (Step 10)
- The Simplification of the Induction Conclusion (Step 10)
- The End of the Flying Tour
- The End of the Flying Tour
- The Base Case in the App Example
- The Base Case in the App Example
- The Simplification of the Induction Conclusion (Step 11)
- The Simplification of the Induction Conclusion (Step 11)
- The Final Simplification in the Base Case (Step 3)
- The Final Simplification in the Base Case (Step 3)
- The Expansion of ENDP in the Induction Step (Step 1)
- The Expansion of ENDP in the Induction Step (Step 1)
- The Expansion of ENDP in the Induction Step (Step 0)
- The Expansion of ENDP in the Induction Step (Step 0)
- The End of the Proof of the Associativity of App
- The End of the Proof of the Associativity of App
- Overview of the Simplification of the Base Case to T
- Overview of the Simplification of the Base Case to T
- The Summary of the Proof of the Trivial Consequence
- The Summary of the Proof of the Trivial Consequence
- The Simplification of the Induction Conclusion (Step 7)
- The Simplification of the Induction Conclusion (Step 7)
- The Simplification of the Induction Conclusion (Step 6)
- The Simplification of the Induction Conclusion (Step 6)
- The Simplification of the Induction Conclusion (Step 5)
- The Simplification of the Induction Conclusion (Step 5)
- The Simplification of the Induction Conclusion (Step 4)
- The Simplification of the Induction Conclusion (Step 4)
- The Simplification of the Induction Conclusion (Step 2)
- The Simplification of the Induction Conclusion (Step 2)
- The Simplification of the Induction Conclusion (Step 0)
- The Simplification of the Induction Conclusion (Step 0)
- The Justification of the Induction Scheme
- The Justification of the Induction Scheme
- The Final Simplification in the Base Case (Step 1)
- The Final Simplification in the Base Case (Step 1)
- The Expansion of ENDP in the Induction Step (Step 2)
- The Expansion of ENDP in the Induction Step (Step 2)
- Popping out of an Inductive Proof
- Popping out of an Inductive Proof
- Overview of the Expansion of ENDP in the Base Case
- Overview of the Expansion of ENDP in the Base Case
- The Simplification of the Induction Conclusion (Step 3)
- The Simplification of the Induction Conclusion (Step 3)
- The Q.E.D. Message
- The Q.E.D. Message
- Overview of the Final Simplification in the Base Case
- Overview of the Final Simplification in the Base Case
- The Final Simplification in the Base Case (Step 2)
- The Final Simplification in the Base Case (Step 2)
- Perhaps
- Perhaps
- Name the Formula Above
- Name the Formula Above
- Undocumented Topic
- Undocumented Topic
- A Trivial Proof
- A Trivial Proof