|
|
|---|
|
|
|
|---|
Papers Involving ACL2
The best introduction to ACL2 is Computer-Aided Reasoning: An Approach; see pubs-books. But if you prefer to read papers on the Web, see the papers listed in the subtopics of this documentation topic. In particular, we recommend the first two papers in pubs-overviews.
Typical formalization problems raise many issues that are not yet adequately addressed in ACL2 (or any other mechanized formal system). If you are trying to formalize a problem in ACL2, you may well have to formalize some ideas for the first time, while extending the work of others. It is often helpful to separate the issues involved in your problem and to try to find papers below that seem likely to touch upon some of those same issues. Then look at those papers for ideas about how to deal with your problems. A comprehensive set of case studies is presented in Computer-Aided Reasoning: ACL2 Case Studies"; see pubs-books.
Several of the papers listed contain links to ACL2 scripts.