Name
Abstract | ||
|---|---|---|
The paper presents a refined method of extracting reasonable and sometimes unexpected programs from classical proofs of formulas of the form ∀x∃yB. We also generalize previously known results, since B no longer needs to be quantifier-free, but only has to belong to a strictly larger class of so-called “goal formulas”. Furthermore we allow unproven lemmas D in the proof of ∀x∃yB, where D is a so-called “definite” formula. |
Year | DOI | Venue |
|---|---|---|
2002 | 10.1016/S0168-0072(01)00073-2 | Annals of Pure and Applied Logic |
Keywords | DocType | Volume |
03F10,03F50 | Journal | 114 |
Issue | ISSN | Citations |
1 | 0168-0072 | 34 |
PageRank | References | Authors |
2.45 | 9 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ulrich Berger | 1 | 151 | 19.55 |
| Wilfried Buchholz | 2 | 159 | 57.31 |
| Helmut Schwichtenberg | 3 | 373 | 44.83 |
| n danner | 4 | 34 | 2.45 |