Switch to: References

Add citations

You must login to add citations.
  1. Learning based realizability for HA + EM1 and 1-Backtracking games: Soundness and completeness.Federico Aschieri - 2013 - Annals of Pure and Applied Logic 164 (6):591-617.
    We prove a soundness and completeness result for Aschieri and Berardiʼs learning based realizability for Heyting Arithmetic plus Excluded Middle over semi-decidable statements with respect to 1-Backtracking Coquand game semantics. First, we prove that learning based realizability is sound with respect to 1-Backtracking Coquand game semantics. In particular, any realizer of an implication-and-negation-free arithmetical formula embodies a winning recursive strategy for the 1-Backtracking version of Tarski games. We also give examples of realizers and winning strategy extraction for some classical proofs. (...)
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • Fluctuations, effective learnability and metastability in analysis.Ulrich Kohlenbach & Pavol Safarik - 2014 - Annals of Pure and Applied Logic 165 (1):266-304.
    This paper discusses what kind of quantitative information one can extract under which circumstances from proofs of convergence statements in analysis. We show that from proofs using only a limited amount of the law-of-excluded-middle, one can extract functionals , where L is a learning procedure for a rate of convergence which succeeds after at most B-many mind changes. This -learnability provides quantitative information strictly in between a full rate of convergence and a rate of metastability in the sense of Tao (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations