File: Nontautological_Subgoals.html

package info (click to toggle)
acl2 3.1-1
  • links: PTS
  • area: main
  • in suites: etch, etch-m68k
  • size: 36,712 kB
  • ctags: 38,396
  • sloc: lisp: 464,023; makefile: 5,470; sh: 86; csh: 47; cpp: 25; ansic: 22
file content (13 lines) | stat: -rw-r--r-- 598 bytes parent folder | download 
1
2
3
4
5
6
7
8
9
10
11
12
13
 
<html>
<head><title>Nontautological_Subgoals.html  --  ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>Prover output omits some details</h2>
<p>
The theorem prover's proof output is intended to suggest an outline
of the reasoning process employed by its proof engine, which is
virtually always more than is necessary for the ACL2 user.  In
particular, the output often omits subgoals that are sufficiently
trivial, including tautologies.
<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>