|
Formal Methods in Computing (Most of the papers antecedent to 1995 are not included in the list) |
|||
| FRAMES NO FRAME | ||||
| Berardi-deLiguoro:CSL-08 (In proceedings) | |
| Author(s) | Stefano Berardi and Ugo de' Liguoro |
| Title | « A Calculus of Realizers for EM1 Arithmetic » |
| In | Proceedings of CSL '08 |
| Series | Lecture Notes in Computer Science |
| Volume | 5213 |
| Page(s) | 215-229 |
| Year | 2008 |
| Publisher | Springer-Verlag |
| Abstract | |
| We propose a realizability interpretation of a system for quantifier free arithmetic which is equivalent to the fragment of classical arithmetic without nested quantifiers, which we call 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 ``environment'' and with each other. With respect to known constructive interpretations of classical arithmetic, the present one differs under many respects: for instance, the interpretation is compositional in a strict sense; in particular the interpretation of (the analogous of) the cut rule is the plain composition of functionals. As an additional remark, any two quantifier-free formulas provably equivalent in classical arithmetic have the same realizer. | |
Download the complete article:
| BibTeX code |
@inproceedings{Berardi-deLiguoro:CSL-08,
volume = {5213},
author = {Stefano Berardi and de' Liguoro, Ugo},
series = {Lecture Notes in Computer Science},
booktitle = {Proceedings of CSL '08},
tag = {{CSL'8}},
localfile = {http://www.di.unito.it/~deligu/pub/RealWFA.pdf},
title = {{A Calculus of Realizers for EM1 Arithmetic}},
abstract = {We propose a realizability interpretation of a system for
quantifier free arithmetic which is equivalent to the fragment of
classical arithmetic without nested quantifiers, which we call
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
``environment'' and with each other. With respect to known
constructive interpretations of classical arithmetic, the present
one differs under many respects: for instance, the interpretation
is compositional in a strict sense; in particular the
interpretation of (the analogous of) the cut rule is the plain
composition of functionals. As an additional remark, any two
quantifier-free formulas provably equivalent in classical
arithmetic have the same realizer.},
publisher = {Springer-Verlag},
year = {2008},
pages = {215-229},
}
|
Formal Methods in Computing (Most of the papers antecedent to 1995 are not included in the list) |
|||
| FRAMES NO FRAME | ||||
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)
