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
|
<html>
<head><title>ACL2_System_Architecture.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>ACL2 System Architecture</h2>
<p>
<img src=acl2-system-architecture.gif><p>
The user interacts with the theorem prover by giving it definitions,
theorems and advice (e.g., ``use this lemma.''), often in the form
of books <a href="BOOKS.html">books</a> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a>.<p>
The theorem prover uses the rules in the library of books the user has
selected.<p>
The theorem prover prints its proof attempts to the user.<p>
When a theorem is proved it is converted to a rule under the control
of the user's <a href="RULE-CLASSES.html">rule-classes</a> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a>.<p>
<b>The informed user can make ACL2 do amazing things.</B><p>
<a href="Rewrite_Rules_are_Generated_from_DEFTHM_Events.html"><img src=walking.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>
|
