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 w.r.t. proofs, in the sense that it is compositional and that it does not need any translation.

Interactive realizers. A new approach to program extraction from non constructive proofs

BERARDI, Stefano;DE' LIGUORO, Ugo
2012-01-01

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 w.r.t. proofs, in the sense that it is compositional and that it does not need any translation.
2012
13 n. 2
1
21
http://dl.acm.org/citation.cfm?id=2159533&CFID=103176599&CFTOKEN=49179530
proof mining; program synthesis
Stefano Berardi; Ugo de'Liguoro
File in questo prodotto:
File Dimensione Formato  
a11-berardi.pdf

Accesso riservato

Tipo di file: PDF EDITORIALE
Dimensione 212.47 kB
Formato Adobe PDF
212.47 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/83690
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 8
  • ???jsp.display-item.citation.isi??? 7
social impact