Data di Pubblicazione:
2010
Abstract:
We associate with any game G another game, which is a variant of it, and which we call bck(G). Winning strategies for bck(G) have a lower recursive degree than winning strategies for G: if a player has a winning strategy of recursive degree 1 over G, then it has a recursive winning strategy over bck(G), and vice versa. Through bck(G) we can express in algorithmic form, as a recursive winning strategy, many (but not all) common proofs of non-constructive Mathematics, namely exactly the theorems of the sub-classical logic Limit Computable Mathematics (Hayashi (2006), Hayashi and Nakata (2001)).
Tipologia CRIS:
03A-Articolo su Rivista
Keywords:
game semantics; backtracking; proof theory
Elenco autori:
Stefano Berardi; Thierry Coquand; Susumu Hayashi
Link alla scheda completa:
Pubblicato in: