Chronological Overview 
 Type-Hierarchical Overview 
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 »
InProceedings of CSL '08
SeriesLecture Notes in Computer Science
Volume5213
Page(s)215-229
Year2008
PublisherSpringer-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: RealWFA.pdf

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},
}


 Chronological Overview 
 Type-Hierarchical Overview 
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)

Valid HTML 4.01!