Name
Title | ||
|---|---|---|
A Constructive Valuation Interpretation for Classical Logic and its Use in Witness Extraction |
Abstract | ||
|---|---|---|
A constructive interpretation of classical arithmetic in terms of a Kripke-like valuation semantics of proofs is presented. We use this interpretation for motivating a constructive procedure, based on reduction rules, for extracting witnesses from proofs of
1
0
sentences in classical arithmetic. |
Year | DOI | Venue |
|---|---|---|
1992 | 10.1007/3-540-55251-0_1 | CAAP |
Keywords | Field | DocType |
classical logic,constructive valuation interpretation,witness extraction | Intuitionistic logic,Discrete mathematics,Computability logic,Paraconsistent logic,Constructive,Complete theory,Mathematical proof,Classical logic,Linear logic,Calculus,Mathematics | Conference |
ISBN | Citations | PageRank |
3-540-55251-0 | 4 | 1.35 |
References | Authors | |
5 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Franco Barbanera | 1 | 357 | 35.14 |
| Stefano Berardi | 2 | 373 | 51.58 |