A Calculus of Realizers for EM 1 Arithmetic (Extended Abstract)

DOI10.1007/978-3-540-87531-4_17MaRDI QIDQ3540181zbMATH OpenOpenAlexFDO

Authors Stefano Berardi, Ugo de'Liguoro

Publication date 20 November 2008

Published in Computer Science Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-87531-4_17

Mathematics Subject Classification ID

First-order arithmetic and fragments (03F30) Computational learning theory (68Q32)

Recommendations

• Interactive realizers: a new approach to program extraction from nonconstructive proofs
• Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM 1
• Interactive learning-based realizability for Heyting arithmetic with \(\mathrm{EM}_1\)
• Interactive realizability for second-order Heyting arithmetic with EM1 and SK1
• Interactive realizability for classical Peano arithmetic with Skolem axioms

Cites work

• A semantics of evidence for classical arithmetic
• Constructivism in mathematics. An introduction. Volume II
• Dependent choice, `quote' and the clock
• scientific article; zbMATH DE number 3503215 (Why is no real title available?)
• scientific article; zbMATH DE number 3614784 (Why is no real title available?)
• scientific article; zbMATH DE number 1324438 (Why is no real title available?)
• scientific article; zbMATH DE number 3334141 (Why is no real title available?)
• Iterated Limiting Recursion and the Program Minimization Problem
• Limiting recursion
• Mathematics based on incremental learning -- excluded middle and inductive inference
• Strong termination for the epsilon substitution method
• The epsilon calculus and Herbrand complexity

Cited in

(6)

• Learning based realizability for HA + EM1 and 1-backtracking games: soundness and completeness
• Interactive learning-based realizability for Heyting arithmetic with \(\mathrm{EM}_1\)
• Interactive realizers: a new approach to program extraction from nonconstructive proofs
• Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM 1
• Interpreting a classical geometric proof with interactive realizability
• Constructive forcing, CPS translations and witness extraction in interactive realizability

This page was built for publication: A Calculus of Realizers for EM 1 Arithmetic (Extended Abstract)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3540181)