Title | ||
---|---|---|
Interactive Realizers: A New Approach to Program Extraction from Nonconstructive Proofs |
Abstract | ||
---|---|---|
We propose a realizability interpretation of a system for quantier free arithmetic which is equivalent to the fragment of classical arithmetic without nested quantifiers, called here EM1-arithmetic. We interpret classical proofs as interactive learning strategies, namely as processes going through several stages of knowledge and learning by interacting with the “nature,” represented by the standard interpretation of closed atomic formulas, and with each other. We obtain in this way a program extraction method by proof interpretation, which is faithful with respect to proofs, in the sense that it is compositional and that it does not need any translation. |
Year | DOI | Venue |
---|---|---|
2012 | 10.1145/2159531.2159533 | ACM Trans. Comput. Log. |
Keywords | Field | DocType |
classical arithmetic,nonconstructive proofs,proof interpretation,interactive realizers,realizability interpretation,program extraction method,standard interpretation,nested quantifiers,program extraction,interactive learning strategy,classical proof,new approach,closed atomic formula,quantier free arithmetic,classical logic | Discrete mathematics,Interactive Learning,Program synthesis,Computer science,Mathematical proof,Proof mining,Realizability | Journal |
Volume | Issue | ISSN |
13 | 2 | 1529-3785 |
Citations | PageRank | References |
6 | 0.57 | 9 |
Authors | ||
2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Stefano Berardi | 1 | 373 | 51.58 |
Ugo de’Liguoro | 2 | 15 | 1.83 |