1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
|
<html>
<head><title>ACL2-TUTORIAL.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h1>ACL2-TUTORIAL</h1>tutorial introduction to ACL2
<pre>Major Section: <a href="acl2-doc-major-topics.html">ACL2 Documentation</a>
</pre><p>
This section contains a tutorial <a href="INTRODUCTION.html">introduction</a> to ACL2, some examples
of the use of ACL2, and pointers to additional information.
<p>
<ul>
<li><h3><a href="INTRODUCTION.html">INTRODUCTION</a> -- introduction to ACL2
</h3>
</li>
<li><h3><a href="STARTUP.html">STARTUP</a> -- How to start using ACL2; the ACL2 <a href="COMMAND.html">command</a> loop
</h3>
</li>
<li><h3><a href="TIDBITS.html">TIDBITS</a> -- some basic hints for using ACL2
</h3>
</li>
<li><h3><a href="TIPS.html">TIPS</a> -- some hints for using the ACL2 prover
</h3>
</li>
<li><h3><a href="TUTORIAL-EXAMPLES.html">TUTORIAL-EXAMPLES</a> -- examples of ACL2 usage
</h3>
</li>
</ul>
You might also find CLI Technical Report 101 helpful for a
high-level view of the design goals of ACL2.<p>
If you are already familiar with Nqthm, see <a href="NQTHM-TO-ACL2.html">nqthm-to-acl2</a> for
help in making the transition from Nqthm to ACL2.<p>
If you would like more familiarity with Nqthm, we suggest CLI
Technical Report 100, which works through a non-trivial example. A
short version of that paper, which is entitled ``Interaction with
the Boyer-Moore Theorem Prover: A Tutorial Study Using the
Arithmetic-Geometric Mean Theorem,'' is to appear in the Journal of
Automated Reasoning's special issue on induction, probably in 1995
or 1996. Readers may well find that this paper indirectly imparts
useful information about the effective use of ACL2.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
