Pages Written Especially for the Tours

Major Section:  ACL2 Documentation

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 specificially for the Web user.

Furthermore, browsing the pages below via the ACL2 :DOC command or via TexInfo is often unsatisfying because those browsers do not support gif files and the notion of 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.

• A Flying Tour of ACL2 -- A Flying Tour of ACL2

• A Sketch of How the Rewriter Works -- A Sketch of How the Rewriter Works

• A Tiny Warning Sign -- A Tiny Warning Sign

• A Trivial Proof -- A Trivial Proof

• A Typical State -- A Typical State

• A Walking Tour of ACL2 -- A Walking Tour of ACL2

• ACL2 Characters -- ACL2 Characters

• ACL2 Conses or Ordered Pairs -- ACL2 Conses or Ordered Pairs

• ACL2 Strings -- ACL2 Strings

• ACL2 Symbols -- ACL2 Symbols

• ACL2 System Architecture -- ACL2 System Architecture

• ACL2 as an Interactive Theorem Prover -- ACL2 as an Interactive Theorem Prover

• ACL2 as an Interactive Theorem Prover (cont) -- ACL2 as an Interactive Theorem Prover (cont)

• ACL2 is an Untyped Language -- ACL2 is an Untyped Language

• About Models -- About Models

• About Types -- About Types

• About the ACL2 Home Page -- About the ACL2 Home Page

• About the Admission of Recursive Definitions -- About the Admission of Recursive Definitions

• About the Prompt -- About the Prompt

• An Example Common Lisp Function Definition -- An Example Common Lisp Function Definition

• An Example of ACL2 in Use -- An Example of ACL2 in Use

• Analyzing Common Lisp Models -- Analyzing Common Lisp Models

• Common Lisp -- Common Lisp

• Common Lisp as a Modeling Language -- Common Lisp as a Modeling Language

• Conversion -- Conversion to Uppercase

• Corroborating Models -- Corroborating Models

• Evaluating App on Sample Input -- Evaluating App on Sample Input

• Flawed Induction Candidates in App Example -- Flawed Induction Candidates in App Example

• Free Variables in Top-Level Input -- Free Variables in Top-Level Input

• Functions for Manipulating these Objects -- Functions for Manipulating these Objects

• Guards -- Guards

• Guessing the Type of a Newly Admitted Function -- Guessing the Type of a Newly Admitted Function

• Guiding the ACL2 Theorem Prover -- Guiding the ACL2 Theorem Prover

• Hey Wait! Is ACL2 Typed or Untyped(Q) -- Hey Wait! Is ACL2 Typed or Untyped?

• How Long Does It Take to Become an Effective User(Q) -- How Long Does It Take to Become an Effective User?

• How To Find Out about ACL2 Functions -- How To Find Out about ACL2 Functions

• How To Find Out about ACL2 Functions (cont) -- How To Find Out about ACL2 Functions (cont)

• Modeling in ACL2 -- Modeling in ACL2

• Models in Engineering -- Models in Engineering

• Models of Computer Hardware and Software -- Models of Computer Hardware and Software

• Name the Formula Above -- Name the Formula Above

• Nontautological Subgoals -- Prover output omits some details

• Numbers in ACL2 -- Numbers in ACL2

• On the Naming of Subgoals -- On the Naming of Subgoals

• Other Requirements -- Other Requirements

• Overview of the Expansion of ENDP in the Base Case -- Overview of the Expansion of ENDP in the Base Case

• Overview of the Expansion of ENDP in the Induction Step -- Overview of the Expansion of ENDP in the Induction Step

• Overview of the Final Simplification in the Base Case -- Overview of the Final Simplification in the Base Case

• Overview of the Proof of a Trivial Consequence -- Overview of the Proof of a Trivial Consequence

• Overview of the Simplification of the Base Case to T -- Overview of the Simplification of the Base Case to T

• Overview of the Simplification of the Induction Conclusion -- Overview of the Simplification of the Induction Conclusion

• Overview of the Simplification of the Induction Step to T -- Overview of the Simplification of the Induction Step to T

• Perhaps -- Perhaps

• Popping out of an Inductive Proof -- Popping out of an Inductive Proof

• Proving Theorems about Models -- Proving Theorems about Models

• Revisiting the Admission of App -- Revisiting the Admission of App

• Rewrite Rules are Generated from DEFTHM Events -- Rewrite Rules are Generated from DEFTHM Events

• Running Models -- Running Models

• Subsumption of Induction Candidates in App Example -- Subsumption of Induction Candidates in App Example

• Suggested Inductions in the Associativity of App Example -- Suggested Inductions in the Associativity of App Example

• Symbolic Execution of Models -- Symbolic Execution of Models

• The Admission of App -- The Admission of App

• The Associativity of App -- The Associativity of App

• The Base Case in the App Example -- The Base Case in the App Example

• The End of the Flying Tour -- The End of the Flying Tour

• The End of the Proof of the Associativity of App -- The End of the Proof of the Associativity of App

• The End of the Walking Tour -- The End of the Walking Tour

• The Event Summary -- The Event Summary

• The Expansion of ENDP in the Induction Step (Step 0) -- The Expansion of ENDP in the Induction Step (Step 0)

• 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 2) -- The Expansion of ENDP in the Induction Step (Step 2)

• The Falling Body Model -- The Falling Body Model

• The Final Simplification in the Base Case (Step 0) -- the Final Simplification in the Base Case (Step 0)

• The Final Simplification in the Base Case (Step 1) -- the Final Simplification in the Base Case (Step 1)

• The Final Simplification in the Base Case (Step 2) -- the Final Simplification in the Base Case (Step 2)

• The Final Simplification in the Base Case (Step 3) -- the Final Simplification in the Base Case (Step 3)

• The First Application of the Associativity Rule -- The First Application of the Associativity Rule

• The Induction Scheme Selected for the App Example -- The Induction Scheme Selected for the App Example

• The Induction Step in the App Example -- The Induction Step in the App Example

• The Instantiation of the Induction Scheme -- The Instantiation of the Induction Scheme

• The Justification of the Induction Scheme -- The Justification of the Induction Scheme

• The Proof of the Associativity of App -- The Proof of the Associativity of App

• The Q.E.D. Message -- The Q.E.D. Message

• The Rules used in the Associativity of App Proof -- The Rules used in the Associativity of App Proof

• The Simplification of the Induction Conclusion (Step 0) -- the Simplification of the Induction Conclusion (Step 0)

• The Simplification of the Induction Conclusion (Step 1) -- the Simplification of the Induction Conclusion (Step 1)

• The Simplification of the Induction Conclusion (Step 10) -- the Simplification of the Induction Conclusion (Step 10)

• The Simplification of the Induction Conclusion (Step 11) -- the Simplification of the Induction Conclusion (Step 11)

• The Simplification of the Induction Conclusion (Step 12) -- the Simplification of the Induction Conclusion (Step 12)

• The Simplification of the Induction Conclusion (Step 2) -- the Simplification of the Induction Conclusion (Step 2)

• The Simplification of the Induction Conclusion (Step 3) -- the Simplification of the Induction Conclusion (Step 3)

• The Simplification of the Induction Conclusion (Step 4) -- the Simplification of the Induction Conclusion (Step 4)

• The Simplification of the Induction Conclusion (Step 5) -- the Simplification of the Induction Conclusion (Step 5)

• The Simplification of the Induction Conclusion (Step 6) -- the Simplification of the Induction Conclusion (Step 6)

• The Simplification of the Induction Conclusion (Step 7) -- the Simplification of the Induction Conclusion (Step 7)

• The Simplification of the Induction Conclusion (Step 8) -- the Simplification of the Induction Conclusion (Step 8)

• The Simplification of the Induction Conclusion (Step 9) -- the Simplification of the Induction Conclusion (Step 9)

• The Summary of the Proof of the Trivial Consequence -- The Summary of the Proof of the Trivial Consequence

• The Theorem that App is Associative -- The Theorem that App is Associative

• The Time Taken to do the Associativity of App Proof -- The Time Taken to do the Associativity of App Proof

• The Tours -- The Tours

• The WARNING about the Trivial Consequence -- The WARNING about the Trivial Consequence

• Undocumented Topic -- Undocumented Topic

• Using the Associativity of App to Prove a Trivial Consequence -- Using the Associativity of App to Prove a Trivial Consequence

• What Is ACL2(Q) -- What Is ACL2?

• What is Required of the User(Q) -- What is Required of the User?

• What is a Mathematical Logic(Q) -- What is a Mathematical Logic?

• What is a Mechanical Theorem Prover(Q) -- What is a Mechanical Theorem Prover?

• What is a Mechanical Theorem Prover(Q) (cont) -- What is a Mechanical Theorem Prover? (cont)

• You Must Think about the Use of a Formula as a Rule -- You Must Think about the Use of a Formula as a Rule