• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Hons-and-memoization
    • Events
    • History
    • Parallelism
    • Programming
    • Start-here
      • Gentle-introduction-to-ACL2-programming
      • ACL2-tutorial
        • Introduction-to-the-theorem-prover
        • Pages Written Especially for the Tours
          • A Tiny Warning Sign
          • About the Prompt
          • ACL2 Symbols
          • Common Lisp
          • About Types
          • The Event Summary
          • An Example of ACL2 in Use
          • The Tours
          • Corroborating Models
          • The Proof of the Associativity of App
          • Guards in ACL2
          • Numbers in ACL2
          • About the Admission of Recursive Definitions
          • Free Variables in Top-Level Input
          • Common Lisp as a Modeling Language
          • ACL2 as an Interactive Theorem Prover (cont)
          • A Flying Tour of ACL2
          • Analyzing Common Lisp Models
          • A Walking Tour of ACL2
          • The Theorem that App is Associative
          • The End of the Walking Tour
          • Proving Theorems about Models
          • Functions for Manipulating these Objects
          • About the ACL2 Home Page
          • ACL2 Conses or Ordered Pairs
          • The Associativity of App
          • Models of Computer Hardware and Software
          • How To Find Out about ACL2 Functions (cont)
          • A Sketch of How the Rewriter Works
          • ACL2 System Architecture
          • Running Models
          • ACL2 is an Untyped Language
          • How To Find Out about ACL2 Functions
          • How Long Does It Take to Become an Effective User(Q)
          • The Admission of App
          • Guiding the ACL2 Theorem Prover
          • What Is ACL2(Q)
          • Conversion
          • An Example Common Lisp Function Definition
          • ACL2 Characters
          • You Must Think about the Use of a Formula as a Rule
          • The WARNING about the Trivial Consequence
          • Guessing the Type of a Newly Admitted Function
          • ACL2 Strings
          • What is a Mathematical Logic(Q)
          • Revisiting the Admission of App
          • What is a Mechanical Theorem Prover(Q)
          • About Models
          • What is Required of the User(Q)
          • Hey Wait! Is ACL2 Typed or Untyped(Q)
          • The Falling Body Model
          • Rewrite Rules are Generated from DEFTHM Events
          • A Typical State
          • The Time Taken to do the Associativity of App Proof
          • The Simplification of the Induction Conclusion (Step 1)
          • The Rules used in the Associativity of App Proof
          • Subsumption of Induction Candidates in App Example
          • Other Requirements
          • Models in Engineering
          • Symbolic Execution of Models
          • Suggested Inductions in the Associativity of App Example
          • Overview of the Proof of a Trivial Consequence
          • Evaluating App on Sample Input
          • The Induction Step in the App Example
          • Modeling in ACL2
          • The Simplification of the Induction Conclusion (Step 9)
          • The Induction Scheme Selected for the App Example
          • The First Application of the Associativity Rule
          • Overview of the Expansion of ENDP in the Induction Step
          • Flawed Induction Candidates in App Example
          • ACL2 as an Interactive Theorem Prover
          • Using the Associativity of App to Prove a Trivial Consequence
          • The Simplification of the Induction Conclusion (Step 8)
          • The Instantiation of the Induction Scheme
          • 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 Conclusion
          • On the Naming of Subgoals
          • Nontautological Subgoals
          • What is a Mechanical Theorem Prover(Q) (cont)
          • The Simplification of the Induction Conclusion (Step 12)
          • The Simplification of the Induction Conclusion (Step 10)
          • The End of the Flying Tour
          • The Base Case in the App Example
          • The Simplification of the Induction Conclusion (Step 11)
          • 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 0)
          • The End of the Proof of the Associativity of App
          • Overview of the Simplification of the Base Case to T
          • The Summary of the Proof of the Trivial Consequence
          • The Simplification of the Induction Conclusion (Step 7)
          • The Simplification of the Induction Conclusion (Step 6)
          • The Simplification of the Induction Conclusion (Step 5)
          • The Simplification of the Induction Conclusion (Step 4)
          • The Simplification of the Induction Conclusion (Step 2)
          • The Simplification of the Induction Conclusion (Step 0)
          • The Justification of the Induction Scheme
          • The Final Simplification in the Base Case (Step 1)
          • The Expansion of ENDP in the Induction Step (Step 2)
          • Popping out of an Inductive Proof
          • Overview of the Expansion of ENDP in the Base Case
          • The Simplification of the Induction Conclusion (Step 3)
          • The Q.E.D. Message
          • Overview of the Final Simplification in the Base Case
          • The Final Simplification in the Base Case (Step 2)
          • Perhaps
          • Name the Formula Above
          • Undocumented Topic
          • A Trivial Proof
        • The-method
        • Advanced-features
        • Interesting-applications
        • Tips
        • Alternative-introduction
        • Tidbits
        • Annotated-ACL2-scripts
        • Startup
        • ACL2-as-standalone-program
        • ACL2-sedan
        • Talks
        • Nqthm-to-ACL2
        • Emacs
      • About-ACL2
    • Real
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Pages Written Especially for the Tours

The Tours

The Tours

ACL2 is a very large, multipurpose system. You can use it as a programming language, a specification language, a modeling language, a formal mathematical logic, or a semi-automatic theorem prover, just to name its most common uses. It has been used on a number of industrial applications. If you're uncertain as to whether your project is appropriate for ACL2 we urge you to look over this list or contact the ACL2 developers.

This home page includes all of ACL2's online documentation, which is quite extensive (over 4 megabytes). To help ease your introduction to ACL2, we have built two tours through this documentation.

If you are familiar with at least some of the industrial applications of ACL2, then you will understand the distance between the simple examples we talk about in these tours and the kinds of things ACL2 users do with the system.

Newcomers to ACL2 should first take the ``Flying Tour.'' Then, if you want to know more, take the ``Walking Tour.'' On your first reading, follow the two Tours linearly, clicking only on the icon of the Tour you're on. Beware of other links, which might jump you from one tour to the other or into the ACL2 User's Manual! Once you've had a coherent overview of the system, you might quickly repeat both Tours to see if there are unvisited links you're interested in, using your browser's Back Button to return to your starting points.

If after all this you want to learn how to use the theorem prover (!), see introduction-to-the-theorem-prover.

To start a tour, click on the appropriate icon below.

If you take the tours in a text-based format (such as using the :DOC command in Emacs), they will probably be unsatisfying because we use gif files and assume you can navigate ``back.''