Name
Abstract | ||
|---|---|---|
We describe a framework with which first order theorem provers can be used for checking formal proofs. The main aim of the framework is to take as much advantage as possible from the strength of first order theorem provers in the formalization of realistic formal proofs. In order to obtain this, we restricted the use of higher order constructs to a minimum. In particular, we refrained fromnotation in formulas and from currying. The first order prover can be freely chosen. All communication with the theorem prover uses TPTP syntax. The system is intended for teaching, for checking mathematical proofs or correctness proofs of algorithms and also for improving the effectiveness of theorem provers. In its current set up, the system is not intended for building large libraries of checked mathematics. |
Year | Venue | Keywords |
|---|---|---|
2008 | PAAR/ESHOL | theorem prover,first order,higher order |
Field | DocType | Citations |
Analytic proof,Discrete mathematics,Computer-assisted proof,Automated theorem proving,Automated proof checking,Mathematical proof,Proof complexity,Gas meter prover,Calculus,Mathematics,Original proof of Gödel's completeness theorem | Conference | 1 |
PageRank | References | Authors |
0.41 | 7 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| hans de nivelle | 1 | 247 | 21.88 |
| Piotr Witkowski | 2 | 13 | 4.09 |