Name
Abstract | ||
|---|---|---|
In informal mathematics, statements involving computations are seldom proved. Instead, it is assumed that readers of the proof can carry out the computations on their own. However, when using an automated proof development system based on type theory, the user is forced to find proofs for all claimed propositions, including computational statements. This paper presents a method to automatically prove statements from primitive recursive arithmetic. The method replaces logical formulas by boolean expressions. A correctness proof is constructed, which states that the original formula is derivable, if and only if the boolean expression equals true. Because the boolean expression reduces to true, the conversion rule yields a trivial proof of the equality. By combining this proof with the correctness proof, we get a proof for the original statement. |
Year | DOI | Venue |
|---|---|---|
2002 | 10.1016/S0304-3975(00)00354-6 | Theor. Comput. Sci. |
Keywords | DocType | Volume |
original formula,logical formula,trivial proof,informal mathematics,computational statement,original statement,Coq system,conversion rule yield,boolean expression,automated proof development system,correctness proof | Journal | 272 |
Issue | ISSN | Citations |
1-2 | Theoretical Computer Science | 5 |
PageRank | References | Authors |
0.72 | 5 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Martijn Oostdijk | 1 | 132 | 13.89 |
| Herman Geuvers | 2 | 457 | 53.92 |