3/26/07

Matt Kaufmann

- To run ACL2 on UT CS linux, start up
`/p/bin/acl2-3.1`

, or to get the latest version (which will likely be updated in 2 or 3 weeks),`/p/bin/acl2`

. - Feel free to sign up for and Use the acl2-help mailing list (available via
links from the
`ACL2 home page.`

- The workhorses of the ACL2 theorem prover are its rewriter and, to some extent, its automated induction>.
- Today's demos:
- LOG FILE
- First demo
- Primary solution to Problem 101
- Alternate solution to Problem 101 using ordinals books.
- Triple-reverse tutorial example:

- We also stressed the use of the documentation

```
```

```
```## Miscellaneous notes

ACL2s (Eclipse interface to
ACL2) may be helpful if you don't know emacs. But if you want to learn emacs,
you might start with this little emacs cheat
sheet.
If you do know emacs, I suggest putting the following in your
`.emacs`

file, and perhaps reading the documentation at the top of
that file.

(load "/projects/acl2/current/emacs/emacs-acl2.el")

For proof trees, see documentation
for topic `proof-tree`

. In a nutshell:

- In emacs:

`meta-x start-proof-tree`

- In ACL2:

`:start-proof-tree`

- Then
`control-z c`

to jump to the next checkpoint.

`:INDUCT`

hints

Suppose we want as an inductive case:
(implies (and (consp x)
(foo (cdr x) (g x y)))
(foo x y))

We can do this:
(defstub g (x y) t)
(defun foo-induction (x y)
(if (consp x)
(foo-induction (cdr x) (g x y))
(list x y)))
(defstub foo (x y) t)
(thm (foo x y)
:hints (("Goal" :induct (foo-induction x y))))