Name
Abstract | ||
|---|---|---|
Experience has shown that large or multi-user interactive proof efforts can benefit significantly from structuring mechanisms, much like those available in many modern programming languages. Such a mechanism can allow some lemmas and definitions to be exported, and others not. In this paper we address two such structuring mechanisms for the ACL2 theorem prover: iencapsulation and ibooks. After presenting an introduction to ACL2, this paper justifies the implementation of ACL2’s structuring mechanisms and, more generally, formulates and proves high-level correctness properties of ACL2. The issues in the present paper are relevant not only for ACL2 but also for other theorem-proving environments. |
Year | DOI | Venue |
|---|---|---|
2001 | 10.1023/A:1026517200045 | J. Autom. Reasoning |
Keywords | DocType | Volume |
first-order logic,automated reasoning,ACL2,constraint,encapsulation,functional instantiation,soundness,Skolemization | Journal | 26 |
Issue | ISSN | Citations |
2 | 1573-0670 | 39 |
PageRank | References | Authors |
2.73 | 7 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Matt Kaufmann | 1 | 206 | 20.16 |
| J. Strother Moore | 2 | 1916 | 526.00 |