Interactive learning based realizability and 1-backtracking games

MaRDI QIDQ4964695zbMATH OpenFDO

Authors Federico Aschieri

Publication date 3 March 2021

Full work available at URL https://arxiv.org/abs/1101.5441, http://eptcs.web.cse.unsw.edu.au/paper.cgi?CLaC10.3

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Relative consistency and interpretations (03F25) First-order arithmetic and fragments (03F30) Intuitionistic mathematics (03F55)

Recommendations

• Learning based realizability for HA + EM1 and 1-backtracking games: soundness and completeness
• 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 classical Peano arithmetic with Skolem axioms
• Interactive realizers: a new approach to program extraction from nonconstructive proofs

Cited in

(6)

• Learning based realizability for HA + EM1 and 1-backtracking games: soundness and completeness
• Specifying Peirce's law in classical realizability
• Realizability for Peano arithmetic with winning conditions in HON games
• Semantics for Intuitionistic Arithmetic Based on Tarski Games with Retractable Moves
• Interpreting a classical geometric proof with interactive realizability
• Classical realizability and arithmetical formulæ

This page was built for publication: Interactive learning based realizability and 1-backtracking games

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