Interactive Realizability for Classical Peano Arithmetic with Skolem Axioms

Federico Aschieri 1
1 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
Abstract : Interactive realizability is a computational semantics of classical Arithmetic. It is based on interactive learning and was originally designed to interpret excluded middle and Skolem axioms for simple existential formulas. A realizer represents a proof/construction depending on some state, which is an approximation of some Skolem functions. The realizer interacts with the environment, which may provide a counter-proof, a counterexample invalidating the current construction of the realizer. But the realizer is always able to turn such a negative outcome into a positive information, which consists in some new piece of knowledge learned about the mentioned Skolem functions. The aim of this work is to extend Interactive realizability to a system which includes classical first-order Peano Arithmetic with Skolem axioms. For witness extraction, the learning capabilities of realizers will be exploited according to the paradigm of learning by levels. In particular, realizers of atomic formulas will be update procedures in the sense of Avigad and thus will be understood as stratified-learning algorithms.
Type de document :
Communication dans un congrès
Computer Science Logic 2012, Sep 2012, Fontainebleau, France. 2012, Computer Science Logic (CSL'12) - 26th International Workshop/21s Annual Conference of the EACSL, 2012, September 3-6, 2012, Fontainebleau, France. 〈10.4230/LIPIcs.CSL.2012.31〉
Liste complète des métadonnées

Littérature citée [17 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00685360
Contributeur : Federico Aschieri <>
Soumis le : samedi 30 juin 2012 - 17:17:30
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : lundi 1 octobre 2012 - 02:21:17

Fichiers

RealizabilityPAfull.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA | PPS | USPC

Citation

Federico Aschieri. Interactive Realizability for Classical Peano Arithmetic with Skolem Axioms. Computer Science Logic 2012, Sep 2012, Fontainebleau, France. 2012, Computer Science Logic (CSL'12) - 26th International Workshop/21s Annual Conference of the EACSL, 2012, September 3-6, 2012, Fontainebleau, France. 〈10.4230/LIPIcs.CSL.2012.31〉. 〈hal-00685360v2〉

Partager

Métriques

Consultations de la notice

281

Téléchargements de fichiers

241