		Search-engine friendly clone of the ACL2 documentation.

ACL2-tutorial

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.

Subtopics

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