Name
Abstract | ||
|---|---|---|
. The ability of a theorem prover to generate explicit derivationsfor the theorems it proves has major benets for the testing andmaintenance of the prover. It also eliminates the need to trust the correctnessof the prover at the expense of trusting a much simpler proofchecker. However, it is not always obvious how to generate explicit proofsin a theorem prover that uses decision procedures whose operation doesnot directly model the axiomatization of the underlying theories. In... |
Year | DOI | Venue |
|---|---|---|
2000 | 10.1007/10721959_3 | CADE |
Keywords | Field | DocType |
touchstone theorem prover,proof generation,theorem prover | Analytic proof,Computer-assisted proof,Discrete mathematics,Computer science,Automated theorem proving,Proof of knowledge,Automated proof checking,Algorithm,Mathematical proof,Gas meter prover,Proof assistant | Conference |
Volume | ISSN | ISBN |
1831 | 0302-9743 | 3-540-67664-3 |
Citations | PageRank | References |
17 | 1.59 | 13 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| George Necula | 1 | 2427 | 180.97 |
| Peter Lee 0001 | 2 | 975 | 147.71 |