Name
Abstract | ||
|---|---|---|
. IVY is a verified theorem prover for first-order logic withequality. It is coded in ACL2, and it makes calls to the theorem proverOtter to search for proofs and to the program MACE to search for countermodels.Verifications of Otter and MACE are not practical becausethey are coded in C. Instead, Otter and MACE give detailed proofs andmodels that are checked by verified ACL2 programs. In addition, theinitial conversion to clause form is done by verified ACL2 code. Theverification... |
Year | DOI | Venue |
|---|---|---|
2000 | 10.1007/10721959_30 | CADE |
Keywords | Field | DocType |
system description,first order logic,theorem prover,programming language | Programming language,Computer science,Automated theorem proving,Algorithm,Mathematical proof,ACL2,Program specification | Conference |
Volume | ISSN | ISBN |
1831 | 0302-9743 | 3-540-67664-3 |
Citations | PageRank | References |
5 | 0.59 | 3 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| William McCune | 1 | 123 | 27.86 |
| Olga Shumsky | 2 | 5 | 0.93 |