Related papers: A Game-Theoretic Computational Interpretation of P…
The present paper introduces a novel notion of `(effective) computability', called viability, of strategies in game semantics in an intrinsic (i.e., without recourse to the standard Church-Turing computability), non-inductive and…
Game Logic is an excellent setting to study proofs-about-programs via the interpretation of those proofs as programs, because constructive proofs for games correspond to effective winning strategies to follow in response to the opponent's…
Game logic is a dynamic modal logic which models strategic two person games; it contains propositional dynamic logic (PDL) as a fragment. We propose an interpretation of game logic based on stochastic effectivity functions. A definition of…
The functional interpretation is a systematic, syntactic method for transforming certain non-constructive proofs into constructive proofs with explicit bounds. We illustrate the interpretation by working through a concrete, fairly simple…
Game semantics aim at describing the interactive behaviour of proofs by interpreting formulas as games on which proofs induce strategies. In this article, we introduce a game semantics for a fragment of first order propositional logic. One…
We introduce operational semantics into games. And based on the operational semantics, we establish a full algebra of games, including basic algebra of games, algebra of concurrent games, recursion and abstraction. The algebra can be used…
Selection of input features such as relevant pieces of text has become a common technique of highlighting how complex neural predictors operate. The selection can be optimized post-hoc for trained models or incorporated directly into the…
We analyze Coquand's game-theoretic interpretation of Peano Arithmetic through the lens of elementary descent recursion. In Coquand's game semantics, winning strategies correspond to infinitary cut-free proofs and cut elimination…
We refine a model for linear logic based on two well-known ingredients: games and simulations. We have already shown that usual simulation relations form a sound notion of morphism between games; and that we can interpret all linear logic…
We develop a correspondence between the theory of sequential algorithms and classical reasoning, via Kreisel's no-counterexample interpretation. Our framework views realizers of the no-counterexample interpretation as dynamic processes…
We investigate the expressive power of a Turing-complete logic based on game-theoretic semantics. By defining suitable fragments and variants of the logic, we obtain a range of natural characterizations for some fundamental families of…
A model checking computation checks whether a given logical sentence is true in a given finite structure. Provenance analysis abstracts from such a computation mathematical information on how the result depends on the atomic data that…
A large body of research is currently investigating on the connection between machine learning and game theory. In this work, game theory notions are injected into a preference learning framework. Specifically, a preference learning problem…
Choice functions constitute a simple, direct and very general mathematical framework for modelling choice under uncertainty. In particular, they are able to represent the set-valued choices that typically arise from applying decision rules…
This paper presents a soundness and completeness proof for propositional intuitionistic calculus with respect to the semantics of computability logic. The latter interprets formulas as interactive computational problems, formalized as games…
We present a game semantics for intuitionistic type theory. Specifically, we propose categories with families of a new variant of games and strategies for both extensional and intensional variants of the type theory with dependent function,…
The present article is a brief informal survey of computability logic --- the game-semantically conceived formal theory of computational resources and tasks. This relatively young nonclassical logic is a conservative extension of classical…
Game semantics provides an interactive point of view on proofs, which enables one to describe precisely their dynamical behavior during cut elimination, by considering formulas as games on which proofs induce strategies. We are specifically…
We use G\"{o}del's Dialectica interpretation to produce a computational version of the well known proof of Ramsey's theorem by Erd\H{o}s and Rado. Our proof makes use of the product of selection functions, which forms an intuitive…
To adequately model mathematical arguments the analyst must be able to represent the mathematical objects under discussion and the relationships between them, as well as inferences drawn about these objects and relationships as the…