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
|
<html>
<head><title>A_Flying_Tour_of_ACL2.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>A Flying Tour of ACL2</h2>
<p>
<img src=large-flying.gif><p>
On this tour you will learn a little about what ACL2 is for rather than how
ACL2 works. At the bottom of the ``page'' (which may extend beyond the end
of your screen) there is a small ``flying tour'' icon. Click on it to go to
the next page of the tour.<p>
The tour visits the following topics sequentially.<p>
<pre>
<b>The Flight Plan</B>
* <a href="About_the_ACL2_Home_Page.html">This Documentation</a>
* <a href="What_Is_ACL2_lparen_Q_rparen_.html">What is ACL2?</a>
* <a href="What_is_a_Mathematical_Logic_lparen_Q_rparen_.html">Mathematical Logic</a>
* <a href="What_is_a_Mechanical_Theorem_Prover_lparen_Q_rparen_.html">Mechanical Theorem Proving</a>
* <a href="About_Models.html">Mathematical Models in General</a>
* <a href="Models_of_Computer_Hardware_and_Software.html">Mathematical Models of Computing Machines</a>
<a href="A_Typical_State.html">Formalizing Models</a>
<a href="Running_Models.html">Running Models</a>
<a href="Symbolic_Execution_of_Models.html">Symbolic Execution of Models</a>
<a href="Proving_Theorems_about_Models.html">Proving Theorems about Models</a>
* Requirements of ACL2
<a href="What_is_Required_of_the_User_lparen_Q_rparen_.html">The User's Skills</a>
<a href="How_Long_Does_It_Take_to_Become_an_Effective_User_lparen_Q_rparen_.html">Training</a>
<a href="Other_Requirements.html">Host System</a>
</pre>
<p>
We intend the tour to take about 10 minutes of your time.
Some pages on the tour contain pointers to other documents.
You need not follow these pointers to stay on the tour.<p>
<a href="About_the_ACL2_Home_Page.html"><img src=flying.gif></a>
<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>
|
