Name
Abstract | ||
|---|---|---|
Different methods for extracting a program from a classical proof are investigated. A direct method based on normalization and the wellknown negative translation combined with a realizability interpretation are compared and shown to yield equal results. Furthermore, the translation method is refined in order to obtain optimized programs. An analysis of the proof translation shows that in many cases only small parts of a classical proof need to be translated. Proofs extracted from such refined translations have simpler type and control structure. The effect of the refinements is demonstrated at two examples. |
Year | DOI | Venue |
|---|---|---|
1994 | 10.1007/3-540-60178-3_80 | LCC |
Keywords | Field | DocType |
classical proofs,program extraction,control structure,direct method | Atomic formula,Direct method,Discrete mathematics,Normalization (statistics),Mathematical proof,Realizability,Mathematics | Conference |
ISBN | Citations | PageRank |
3-540-60178-3 | 19 | 2.72 |
References | Authors | |
3 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ulrich Berger | 1 | 197 | 18.25 |
| Helmut Schwichtenberg | 2 | 373 | 44.83 |