How do I “steer” ACL2/ACL2s ?

People have wanted to know how to steer ACL2 more precisely. Often the best and most useful advice is to try and “proof-sketch” your conjecture ahead of time, (like a professional) see what lemmata you need, and so forth.

In terms of the mechanics of reading through an ACL2 log, my advice is:

1. Don’t panic
2. I have linked you to some nice walk-through documentation of what to /do/ with a log
3. The ACL2 website also has a nice interactive tutorial.
4. You might also see Pete’s chapter on the subject.

But my advice is strongly to work with rewrite rules and inductive proofs. Those are methods of reasoning that I understand and ways that I know to use the tool, and I avoid the esoteric until it becomes necessary.