How the theorem prover works — level 0

Software is complex, and ACL2 is a piece of software that is used to analyze software — adding another layer of complexity. Furthermore, instead of being limited to static analysis for certain fixed properties, ACL2 allows you — indeed, forces you — to formalize the problem and the questions. It ``knows'' nothing inherent about your problem before you start to interact with it. But it can be used to help answer the most complicated questions you can ask about software.

All this is to say that it is not the kind of tool that you just install and then start to use effectively. So OK, you've installed it or confirmed that you can invoke it. Good for you. Now you have to learn how to use it! Your success ultimately comes down to your understanding of your problem domain and your appropriate exploitation of ACL2's strengths and avoidance of its weaknesses. So put aside the idea of sitting down and interacting with it. Instead, learn about it.

We assume you know some of the

If you haven't visited these links, please do so now.

This tutorial will take you several hours — maybe several days
— to work through. Do not breeze through it as you might a blog.
*Think* your way through it. *Remember* what you read. Do not take
short cuts. If you start to use ACL2 before you really know how, it will only
frustrate you.

We recommend that you read this tutorial with an HTML browser so that you can see which links you've followed and which you have not. To give you a sense of what is in store, here is a map of this document. But don't navigate through it from here! Read it linearly, following the links when the text directs you to.

introduction-to-the-theorem-prover introduction-to-rewrite-rules-part-1 special-cases-for-rewrite-rules equivalent-formulas-different-rewrite-rules introduction-to-key-checkpoints dealing-with-key-combinations-of-function-symbols generalizing-key-checkpoints post-induction-key-checkpoints introduction-to-rewrite-rules-part-2 strong-rewrite-rules practice-formulating-strong-rules practice-formulating-strong-rules-1 practice-formulating-strong-rules-2 practice-formulating-strong-rules-3 practice-formulating-strong-rules-4 practice-formulating-strong-rules-5 practice-formulating-strong-rules-6 specific-kinds-of-formulas-as-rewrite-rules further-information-on-rewriting introduction-to-the-database introduction-to-hints introduction-to-a-few-system-considerations introductory-challenges introductory-challenge-problem-1 introductory-challenge-problem-2 introductory-challenge-problem-3(there are others but at least do a few)frequently-asked-questions-by-newcomers

If any of the links above are marked as ``visited'' by your browser, use
your browser's tools menu to mark all links as unvisited. As you can see, we
really think you'll get the most out of this document if you take it
seriously. As you read, you will see some links to ``advanced'' topics.
These are marked with a tiny warning sign, ``*not* visit any of these advanced links
until you have read the entire tutorial at least once.

After you finish this tutorial material, we recommend that you look at the ACL2 Demos, at the ``Demos'' link of the ACL2 home page.

Most users of ACL2 have bought the book

*Computer-Aided Reasoning: An Approach*, Kaufmann, Manolios, and
Moore, Kluwer Academic Publishers, June, 2000

which is available in paperback from Lulu for approximately $20 (as of 2010). That book contains hundreds of exercises in programming, proof, and using The Method described here to prove theorems. Solutions to the exercises are online, as are appendices that focus on some practical usage aspects. See this web page about the book, which also includes information about its companion (also available on Lulu) describing applications of ACL2, some of which are from industry.

Using ACL2 is akin to having a partner in the theorem proving enterprise. It will do some of the work and you will do some of the work. It can't really be any other way because theorem proving is undecidable. You bring a quirky, error-prone, creative insight to the problem, and ACL2 brings accuracy, logic, and perseverance.

Here we describe a ``model'' of how the system works and introduce some of the ideas and terminology you'll use repeatedly when interacting with it.

This article is about the *theorem prover* itself, not the programming
language and not the logic. We assume you know enough about the ACL2
programming language that you can define simple functions, run them, and read
and write ACL2 constants and terms. For some examples of what we'll take for
granted about ACL2 programming, see programming-knowledge-taken-for-granted.

We also assume you know enough about logic to understand, for example, the words we use to talk about formulas and proofs. To see some examples of what we'll take for granted about your knowledge of logic terminology, see logic-knowledge-taken-for-granted.

When you give the theorem prover a goal formula to prove, it tries to prove
it by breaking it down into subgoals, each of which must be proved in order to
prove the original goal. This breaking apart of the goal is done by various
*proof techniques* built into ACL2. Different proof techniques break the
formula apart in different ways. For example, the *simplifier* rips
apart the propositional structure to isolate the various cases and applies
rewrite rules to simplify the subterms of the formula, while the
*induction* *engine* will attempt to break the goal into some base
cases and some induction steps.

The theorem prover's behavior is affected by a *database* of
*rules* derived from axioms, definitions, and previously proved theorems.
The database also records the *enabled status* of each rule; only enabled
rules are seen by the prover and you can set the status of a rule. There are
many other user-settable switches and parameters affecting the behavior of the
prover; you'll learn about some of them later.

You guide the theorem prover most of the time simply by identifying lemmas
for it to prove. (A *lemma* is just a theorem that you think is useful
in the proofs of other theorems.)

Why does this guide the theorem prover? Because every time you get the
system to prove a theorem, it turns the theorem into a rule (unless you tell
it not to) and stores the rule in the database. That changes how the prover
behaves subsequently. But *you* determine the kind of rule ACL2
stores.

To learn to ``drive'' the theorem prover you have to learn how various rules affect the system's behavior and how it turns proved formulas into rules. But before we discuss this, we discuss a more mathematical activity: how do you figure out the lemmas ACL2 will need in order for it to prove interesting theorems? ACL2 can often help you in this activity, if you use it in the right way.

Here is the way we recommend you use ACL2.

**The Method**.

(1) you present ACL2 with the goal conjecture to prove

(2) typically, it fails to prove it (or you abort its attempt), but it
prints some *Key Checkpoints*

(3) you look at the Key Checkpoints and decide that you know a fact that will help; this tutorial will present some helpful questions to keep in mind

(4) you formalize your knowledge as a formula, along with directions for
how ACL2 should turn the formula into a rule; this tutorial will tell you
about the most commonly used rule, the *rewrite* rule

(5) you recursively apply The Method to get ACL2 to prove your formula and to store it as the kind of rule you specified

(6) go to step (1)

Caveat: This approach simply won't work on some theorems! Basically, this is a ``troubleshooting'' approach, where you're letting ACL2 determine the basic strategy and you're just helping with the subgoals. But for some theorems, ACL2's approach will be misguided and no amount of troubleshooting will salvage its strategy. You'll have a sense that this is happening when it happens because the formulas ACL2 presents to you will raise issues that feel irrelevant to you. The basic truth is that if you think a formula is always true there are usually strong intuitive reasons behind your belief. If you were asked to defend your belief, you'd start to explain your reasons and with training you can turn that into a proof. So when ACL2's formulas present you with things you haven't thought of either (a) you'll have an ``Ah ha!'' moment when you realize you hadn't considered that case or (b) you'll realize that ACL2's approach is different from your intuitive ``proof.''

But, surprisingly often, the troubleshooting approach to finding proofs
works quite well, especially as you rein in your expectations and develop a
sense of what ACL2 can handle on its own. Of course, if you can decompose the
proof into a couple of main lemmas before you start, so much the better: write
down your sequence of lemmas, thinking about the rules you want them to
generate, and get ACL2 to prove each of them before giving it the main
theorem. This *proof planning* approach will gradually become an
integral part of your use of The Method.

The only mechanized help we can offer with The Method, aside from the theorem prover itself, are tools to help you manage the stack of subgoals it generates when, in step (5) you recursively apply The Method to a lemma. There are both Emacs and Eclipse tools available.

To use The Method you have to read the Key Checkpoints printed at the very
end of *failed* proof attempts, just after the line that reads:

The key checkpoint goals, below, may help you to debug this failure.

Most users do not read the output from successful proofs and do not read
the output *during* a proof — they just let it stream by as a sort
of gestalt meter on the theorem prover's progress or lack thereof. For
example, you'll be able to tell it is in a loop and needs to be
interrupted.

You will respond to most Key Checkpoints by formulating new lemmas for the
system to prove and store as rules designed by you to alter ACL2's behavior so
that it proves the Key Checkpoints. You will give each lemma a *name*
and write some *formula* to express the mathematical idea. You'll
command ACL2 to prove it by typing:

(defthmnameformula...)

In the ``...'' you may provide two other kinds of information: *hints*
for how to prove *formula* and directives, called *rule-classes*,
for how to convert *formula* into a rule after it has proved
*formula*. Note that *you* are in charge of determining what kind
of rule ACL2 generates! There are over a dozen different types of rules with
many opportunities to specialize each type. But the most common kind of rule
you'll want to generate is a *rewrite* rule.

We recommend that you read the following topics in the following order,
without skipping anything except links into the ACL2 User's Manual, which are
marked by the little warning sign, ``

(1) See introduction-to-rewrite-rules-part-1 to read about the use and design of rewrite rules.

(2) See introduction-to-key-checkpoints to see how to use The Method to help you design rules.

(3) See introduction-to-rewrite-rules-part-2 for general guidance on how to turn formulas into effective rules.

(4) See introduction-to-the-database to see how to issue commands that build different kinds of rules and that affect the enabled status of existing rules.

(5) See introduction-to-hints to see how to give the prover hints for how to prove specific theorems or even subgoals of specific proof attempts.

(6) See introduction-to-a-few-system-considerations for a few words about system aspects of interacting with ACL2.

(7) See introductory-challenges for a graduated sequence of good
challenge problems for the new user to tackle. **Do not skip this
section!** It is here that you *really* learn how to use ACL2 —
by using it.

(8) See frequently-asked-questions-by-newcomers for a list of questions that new users frequently ask, answered mainly by providing links into the ACL2 User's Manual. We recommend that you skim through these questions and remember that you can find the answers here later. We are very interested in receiving suggestions for how to improve this FAQ and this tutorial. See the ACL2 home page, specifically the link ``Mailing Lists''.

Please read all of the material cited above (skipping only the ACL2 User's
Manual links (``

By this point you should have read, at least, the following topics from this tutorial introduction to the theorem prover:

introduction-to-the-theorem-prover introduction-to-rewrite-rules-part-1 special-cases-for-rewrite-rules equivalent-formulas-different-rewrite-rules introduction-to-key-checkpoints dealing-with-key-combinations-of-function-symbols generalizing-key-checkpoints post-induction-key-checkpoints introduction-to-rewrite-rules-part-2 strong-rewrite-rules practice-formulating-strong-rules practice-formulating-strong-rules-1 practice-formulating-strong-rules-2 practice-formulating-strong-rules-3 practice-formulating-strong-rules-4 practice-formulating-strong-rules-5 practice-formulating-strong-rules-6 specific-kinds-of-formulas-as-rewrite-rules further-information-on-rewriting introduction-to-the-database introduction-to-hints introduction-to-a-few-system-considerations introductory-challenges introductory-challenge-problem-1 introductory-challenge-problem-2 introductory-challenge-problem-3(there are others but at least do a few)frequently-asked-questions-by-newcomers

We also recommend that you look at the ACL2 Demos mentioned in the ACL2-tutorial.

Most users of ACL2 have bought the book

*Computer-Aided Reasoning: An Approach*, Kaufmann, Manolios, and
Moore, Kluwer Academic Publishers, June, 2000

which is available in paperback from Lulu for approximately $20 (as of 2010). That book contains hundreds of exercises in programming, proof, and using The Method to prove theorems. Solutions to the exercises are online. See also this web page about the book, which also includes information about its companion (also available on Lulu) describing applications of ACL2, some of which are from industry.

Thank you for spending the time to get acquainted with the basics of the ACL2 theorem prover. Don't hesitate to send further questions to the ACL2 Help address on the ``Mailing Lists'' link of the ACL2 home page.

**End of Tutorial Introduction to the Theorem Prover**

Below is a list of all of the topics cited on this page.

- Logic-knowledge-taken-for-granted
- Background knowledge in ACL2 logic for theorem prover tutorial
- Logic-knowledge-taken-for-granted-inductive-proof
- A brief explanation of induction
- Introduction-to-rewrite-rules-part-1
- Introduction to ACL2's notion of rewrite rules
- Introduction-to-key-checkpoints
- What questions to ask at key checkpoints
- Logic-knowledge-taken-for-granted-propositional-calculus
- A brief explanation of propositional calculus
- Introduction-to-rewrite-rules-part-2
- How to arrange rewrite rules
- Introduction-to-a-few-system-considerations
- The mechanics of interaction with the theorem prover
- Introduction-to-the-database
- How to update the database
- Programming-knowledge-taken-for-granted
- Background knowledge in ACL2 programming for theorem prover tutorial
- Logic-knowledge-taken-for-granted-rewriting
- A brief explanation of rewriting from the logical perspective
- Introductory-challenge-problem-4-answer
- Answer to challenge problem 4 for the new user of ACL2
- Introduction-to-programming-in-ACL2-for-those-who-know-lisp
- Introduction to programming in ACL2 for Lisp users
- Introduction-to-hints
- How to provide hints to the theorem prover
- Dealing-with-key-combinations-of-function-symbols
- How to get rid of key combinations of function symbols
- Architecture-of-the-prover
- A simple overview of how the prover works
- Further-information-on-rewriting
- A grab bag of advice and information on rewriting
- Frequently-asked-questions-by-newcomers
- Some questions newcomers frequently ask
- Specific-kinds-of-formulas-as-rewrite-rules
- Advice about how to handle commonly occurring formulas as rewrite rules
- Strong-rewrite-rules
- Formulating good rewrite rules
- Practice-formulating-strong-rules-3
- Rules suggested by
(MEMBER (FOO A) (APPEND (BAR B) (MUM C))) - Practice-formulating-strong-rules-1
- Rules suggested by
(TRUE-LISTP (APPEND (FOO A) (BAR B))) - Generalizing-key-checkpoints
- Getting rid of unnecessary specificity
- Logic-knowledge-taken-for-granted-q1-answer
- The inductive step of the
rev-rev proof — Answer to Question 1 - Practice-formulating-strong-rules-6
- Rules suggested by
(MEMBER (FOO A) (NATS-BELOW (BAR B))) - Example-inductions
- Some examples of induction schemes in ACL2
- Logic-knowledge-taken-for-granted-q2-answer
- The inductive step of the
rev-rev proof — Answer to Question 2 - Logic-knowledge-taken-for-granted-rewriting-repeatedly
- Further information on expanding definitions via rewriting
- Introductory-challenge-problem-4
- Challenge problem 4 for the new user of ACL2
- Equivalent-formulas-different-rewrite-rules
- Logically equivalent formulas can generate radically different rules
- Post-induction-key-checkpoints
- Reading post-induction key checkpoints
- Special-cases-for-rewrite-rules
- Convenient short forms for rewrite rule formulas
- Example-induction-scheme-with-accumulators
- Induction scheme with accumulators
- Practice-formulating-strong-rules-5
- Rules suggested by
(SUBSETP (FOO A) (APPEND (BAR B) (MUM C))) - Practice-formulating-strong-rules
- A few simple checkpoints suggesting strong rules
- Practice-formulating-strong-rules-2
- Rules suggested by
(TRUE-LISTP (REV (FOO A))) - Introductory-challenges
- Challenge problems for the new ACL2 user
- Logic-knowledge-taken-for-granted-equals-for-equals
- Substitution of equals for equals
- Logic-knowledge-taken-for-granted-evaluation
- Evaluation during proofs
- Example-induction-scheme-nat-recursion
- Induction on natural numbers
- Example-induction-scheme-down-by-2
- Induction downwards 2 steps at a time
- Logic-knowledge-taken-for-granted-instance
- A brief explanation of substitution instances
- Introductory-challenge-problem-3-answer
- Answer to challenge problem 3 for the new user of ACL2
- Example-induction-scheme-on-lists
- Induction on lists
- Example-induction-scheme-upwards
- Induction upwards
- Example-induction-scheme-with-multiple-induction-steps
- Induction scheme with more than one induction step
- Practice-formulating-strong-rules-4
- Rules suggested by
(SUBSETP (APPEND (FOO A) (BAR B)) (MUM C)) - Logic-knowledge-taken-for-granted-q3-answer
- The inductive step of the
rev-rev proof — Answer to Question 2 - Example-induction-scheme-binary-trees
- Induction on binary trees
- Introductory-challenge-problem-3
- Challenge problem 3 for the new user of ACL2
- Introductory-challenge-problem-1
- Challenge problem 1 for the new user of ACL2
- Logic-knowledge-taken-for-granted-base-case
- A brief explanation of base cases
- Introductory-challenge-problem-1-answer
- Answer to challenge problem 1 for the new user of ACL2
- Example-induction-scheme-on-several-variables
- Induction on several variables
- Introductory-challenge-problem-2-answer
- Answer to challenge problem 2 for the new user of ACL2
- Introductory-challenge-problem-2
- Challenge problem 2 for the new user of ACL2