Sciweavers

TLCA
2009
Springer
13 years 11 months ago
Relating Classical Realizability and Negative Translation for Existential Witness Extraction
Friedman showed how to turn a classical proof of a Σ0 1 formula into an intuitionistic proof of the same formula, thus giving an effective method to extract witnesses from classi...
Alexandre Miquel