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
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
|
<HTML>
<HEAD><TITLE>ACL2 Version 3.1</TITLE></HEAD>
<BODY TEXT="#000000" BGCOLOR="#FFFFFF">
<TABLE>
<TR>
<TD>
<IMG SRC="logo.gif" ALIGN=LEFT ALT="ACL2">
</TD>
<TD>
<CENTER><H1>ACL2 Version 3.1</H1></CENTER>
ACL2 is both a programming language in which you can model computer systems
and a tool to help you prove properties of those models.<P>
ACL2 is part of the Boyer-Moore family of provers, for which its authors have
received the 2005 <A HREF="http://awards.acm.org/software_system/">ACM
Software System Award</A>.<P>
<CENTER><H3><I><A HREF="http://www.cs.utexas.edu/users/moore/acl2/admin/forms/search.html">SEARCH</A></I></H3></CENTER>
</TD>
</TR>
</TABLE>
<HR>
<TABLE CELLPADDING=3>
<TR>
<TD ALIGN=CENTER VALIGN=MIDDLE>
<A HREF="The_Tours.html"><IMG SRC="door02.gif" BORDER=0></A>
</TD>
<TD>
<A HREF="The_Tours.html">Tours</A> and <A HREF="http://www.cs.utexas.edu/users/moore/publications/demos.html">demos</A>
</TD>
<TD ALIGN=CENTER VALIGN=MIDDLE>
<A HREF="http://www.cs.utexas.edu/users/moore/acl2/workshops.html"><IMG SRC="teacher2.gif" BORDER=0></A>
</TD>
<TD>
<A HREF="http://www.cs.utexas.edu/users/moore/acl2/workshops.html">ACL2 Workshops, UT ACL2 Seminar, and Upcoming Conferences</A>
</TD>
<!--
The Workshops entry was added in place of the FAQ entry.
The FAQ was added in place of the one removed by this comment.
At one time we had a link to the tutorials. But after the publication
of the first book, we decided that we should encourage people to read the
book rather than do the tutorials, which are not elementary enough.
I think we should write some appropriate tutorials. Meanwhile, this
entry is left blank.
<TD ALIGN=CENTER VALIGN=MIDDLE>
<A HREF="ACL2-TUTORIAL.html"><IMG SRC="teacher2.gif" BORDER=0></A>
</TD>
<TD>
<A HREF="ACL2-TUTORIAL.html">Tutorials (for those who have taken the tours)</A>
</TD>
-->
</TR>
<TR>
<TD ALIGN=CENTER VALIGN=MIDDLE>
<A HREF="http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html">
<IMG SRC="doc03.gif" BORDER=0></A>
</TD>
<TD>
<A HREF="http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html">
Books and Papers about ACL2 and Its Applications</A>
</TD>
<TD ALIGN=CENTER VALIGN=MIDDLE>
<A HREF="#User's-Manual"><IMG SRC="info04.gif" BORDER=0></A>
</TD>
<TD>
<A HREF="#User's-Manual">The User's Manual</A>
and <A HREF="http://www.cs.utexas.edu/users/moore/publications/hyper-card.html">Hyper-Card</A>
</TD>
</TR>
<TR>
<TD ALIGN=CENTER VALIGN=MIDDLE>
<A HREF="#Tools"><img src="tools3.gif" BORDER=0></A>
</TD>
<TD>
<A HREF="#Tools">Mathematical Tools (Lemma Libraries and Utilities); and, How
to Contribute</A>
</TD>
<TD ALIGN=CENTER VALIGN=MIDDLE>
<!-- This relative URL is made absolute in distributed tar file -->
<A HREF="http://www.cs.utexas.edu/users/moore/acl2/v3-1/installation.html#Addresses"><img src="mailbox1.gif" BORDER=0></A>
</TD>
<TD>
<!-- This relative URL is made absolute in distributed tar file -->
<A HREF="http://www.cs.utexas.edu/users/moore/acl2/v3-1/installation.html#Addresses">Mailing Lists</A>
</TD>
</TR>
<TR>
<TD ALIGN=CENTER VALIGN=MIDDLE>
<!-- This relative URL is made absolute in distributed tar file -->
<A HREF="http://www.cs.utexas.edu/users/moore/acl2/v3-1/new.html">
<IMG SRC="new04.gif" BORDER=0></A>
</TD>
<TD>
<!-- This relative URL is made absolute in distributed tar file -->
<A HREF="http://www.cs.utexas.edu/users/moore/acl2/v3-1/new.html">
Recent changes to this page</A>
</TD>
<TD ALIGN=CENTER VALIGN=MIDDLE>
<!-- This relative URL is made absolute in distributed tar file -->
<A HREF="http://www.cs.utexas.edu/users/moore/acl2/v3-1/installation.html"><img src="ftp2.gif" BORDER=0></A>
</TD>
<TD>
<!-- This relative URL is made absolute in distributed tar file -->
<A HREF="http://www.cs.utexas.edu/users/moore/acl2/v3-1/installation.html">Obtaining and Installing Version 3.1</A>
</TD>
</TR>
<TR>
<TD ALIGN=CENTER VALIGN=MIDDLE>
<A HREF="NOTE-3-1.html"><IMG SRC="note02.gif" BORDER=0></A>
</TD>
<TD>
<A HREF="NOTE-3-1.html">Differences with Version 3.0</A><A HREF="A_Tiny_Warning_Sign.html"> <IMG SRC="twarning.gif"></A>
</TD>
<TD ALIGN=CENTER VALIGN=MIDDLE>
<A HREF="http://www.cs.utexas.edu/users/moore/acl2/v2-9/acl2-doc.html">
<img src="file04.gif" BORDER=0></A>
</TD>
<TD>
<A HREF="other-releases.html">
Other Releases</A>
</TD>
</TR>
<TR>
<TD ALIGN=CENTER VALIGN=MIDDLE></TD>
<TD NOWRAP>
<B><A HREF="mailto:kaufmann@cs.utexas.edu">Matt Kaufmann</A> and <A HREF="mailto:moore@cs.utexas.edu">J Strother Moore</A></B><BR>
<A HREF="http://www.utexas.edu">University of Texas at Austin</A><BR>
November 28, 2006
</TD>
<TD ALIGN=CENTER VALIGN=MIDDLE></TD>
<TD>
<BR><BR>
We gratefully acknowledge substantial support from the following.
(These are included in a much more complete <A
href="ACKNOWLEDGMENTS.html">acknowledgments page</A>.)
<UL>
<LI>DARPA</LI>
<LI>National Science Foundation (Any opinions, findings and conclusions or recomendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation (NSF).)</LI>
<LI>Advanced Micro Devices, Inc.</LI>
<LI>Rockwell Collins, Inc.</LI>
<LI>Sun Microsystems, Inc.</LI>
</UL>
</TD>
</TR>
</TABLE>
<BR><BR><HR><BR><BR>
<H2><A NAME="User's-Manual">The User's Manual</A></H2>
ACL2's user manual is a vast hypertext document. You can wander through
it here, in its HTML format.
<P>
Here are the two common entries to the documentation graph:
<TABLE CELLPADDING=3>
<TR>
<TD ALIGN=CENTER VALIGN=MIDDLE>
<A HREF="acl2-doc-major-topics.html"><IMG SRC="file03.gif" BORDER=0></A>
</TD>
<TD>
<A HREF="acl2-doc-major-topics.html">Major Topics (Table of Contents)</A>
<A HREF="A_Tiny_Warning_Sign.html"><IMG SRC="twarning.gif"></A>
</TD>
</TR>
<TR>
<TD ALIGN=CENTER VALIGN=MIDDLE>
<A HREF="acl2-doc-index.html">
<IMG SRC="index.gif" BORDER=0></A>
</TD>
<TD>
<A HREF="acl2-doc-index.html">Index of all documented topics</A> <A HREF="A_Tiny_Warning_Sign.html"><IMG SRC="twarning.gif"></A>
</TD>
</TR>
</TABLE>
The tiny warning signs, <A HREF="A_Tiny_Warning_Sign.html"><IMG SRC="twarning.gif"></A>, indicate that the links lead out of
introductory level material and into user-level material. It is easy for the
newcomer to get lost.
<P>
Here is how we recommend you use this documentation.
<P>
If you are a newcomer to ACL2, we do <EM>not</EM> recommend that you wander off
into the full documentation. Instead start with
<A HREF="The_Tours.html">the tours</A> and perhaps <A
HREF="http://www.cs.utexas.edu/users/moore/publications/demos.html">the
demos</A>.<P>
If you are still interested in ACL2, we recommend that you get a copy of
<A HREF="http://www.cs.utexas.edu/users/moore/publications/acl2-books/car/index.html">Computer-Aided Reasoning: An Approach</A> and read it carefully. Work
the exercises with ACL2. Learn ``The Method.''<P>
Less effective than reading the book and doing the exercises, but
still useful, is to read selected papers from <A
HREF="http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html">
Books and Papers about ACL2 and Its Applications</A>,
read the documentation topic <A HREF="THE-METHOD.html">the-method</A><A HREF="A_Tiny_Warning_Sign.html"><IMG SRC="twarning.gif"></A>,
and the <A HREF="http://www.cs.utexas.edu/users/moore/publications/hyper-card.html">Hyper-Card</A>
and then work
your way through <A HREF="ACL2-TUTORIAL.html">the tutorials</A>.<P>
Then, we recommend you
read selected topics from ``Major Topics'': <UL>
<LI><A HREF="EVENTS.html">EVENTS</A>
<A HREF="A_Tiny_Warning_Sign.html"><IMG SRC="twarning.gif"></A>
-- the top-level commands like <CODE>DEFUN</CODE> and <CODE>DEFTHM</CODE>
<LI><A HREF="PROGRAMMING.html">PROGRAMMING</A>
<A HREF="A_Tiny_Warning_Sign.html"><IMG SRC="twarning.gif"></A>
-- all the Common Lisp functions ACL2 supports
<LI><A HREF="RULE-CLASSES.html">RULE-CLASSES</A>
<A HREF="A_Tiny_Warning_Sign.html"><IMG SRC="twarning.gif"></A>
-- how you can influence ACL2's behavior with rules,
<LI><A HREF="BOOKS.html">BOOKS</A>
<A HREF="A_Tiny_Warning_Sign.html"><IMG SRC="twarning.gif"></A>
-- how to create re-usable databases of rules.
</UL>
<P>
Finally, experienced users tend mostly to use the ``Index'' to lookup concepts
mentioned in error messages or vaguely remembered from their past experiences
with ACL2.
<P>
<B>Note</B>: If ACL2 has been installed on your local system, the HTML documentation
should also be available locally. You can minimize network traffic by
browsing your local copy. Suppose ACL2 was installed on
<CODE>/usr/jones/acl2/vi-j</CODE>. Then the local URL for this page is
<BR><CODE>file:/usr/jones/acl2/vi-j/acl2-sources/doc/HTML/acl2-doc.html</CODE>.<BR>
Many ACL2 users set a browser bookmark to this file and use their browser to
access the documentation during everyday use of ACL2. If you obtain ACL2,
please encourage users to use the local copy of the documentation rather than
access it across the Web.
<P>
<B>Note</B>: The documentation is available in four forms: Postscript (which
prints as a book over 1200 pages long), HTML, EMACS Texinfo, and ACL2's own
:DOC commands. The documentation, in all but the Postscript form, is
distributed with the source code for the system. So if you have already
obtained ACL2, you should look in the <CODE>doc/</CODE> subdirectory of the
directory upon which ACL2 is installed. You may obtain the gzipped Postscript
form of the documentation by clicking <A HREF=
"http://www.cs.utexas.edu/users/moore/publications/acl2-book.ps.gz">here (1.4
MB)</A>.
<BR><HR><BR>
<H2><A NAME="Tools">Mathematical Tools</A></H2>
The distribution of ACL2 includes some tools built by users. Most of
these are ACL2 ``<A
HREF="http://www.cs.utexas.edu/users/moore/acl2/v3-1/distrib/acl2-sources/books/Readme.html">books</A>,''
which are collections of definitions and theorems you might find
useful in your models and proofs. Most of the available books come with the distribution, but
the above link will also take you to additional books in support of the ACL2
Workshops (``<code>workshops</code>'') and non-standard analysis
(``<code>nonstd</code>'').
<p>
We strongly encourage users to submit additional books by following the <A
HREF="http://www.cs.utexas.edu/users/moore/acl2/books/index.html">instructions for contributing books to ACL2</A>.
<p>
We also distribute a few interface
tools, such as support for infix printing. For these, see the <A
HREF="http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html#Utilities">Utilities</A>
section of <A HREF=
"http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html">
Books and Papers about ACL2 and Its Applications</A>. Some of the
papers mentioned in that collection contain utilities, scripts, or
ACL2 books the problem domains in question.
<BR><HR><BR><BR><BR><BR><BR><BR>
</BODY>
</HTML>
|
