1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
<html>
<head><title>Guiding_the_ACL2_Theorem_Prover.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>Guiding the ACL2 Theorem Prover</h2>
<p>
Now that you have seen the theorem prover in action you might be
curious as to how you guide it.<p>
<img src=interactive-theorem-prover.gif><p>
The idea is that the user submits conjectures and advice and
reads the proof attempts as they are produced.<p>
Most of the time, the conjectures submitted are <b>lemmas</B> to be
used in the proofs of other theorems.<p>
<a href="ACL2_as_an_Interactive_Theorem_Prover__lparen_cont_rparen_.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>
|
