Propositional Games with Explicit Strategies

This paper introduces a game-theoretic semantics for LP, Artemov's Logic of Proofs, taking the viewpoint that LP is a logic of explicit strategies on propositional verification games. To demonstrate the utility of this viewpoint, we define an embedding of the well-known game of Nim into the propositional verification game, which allows us to extract a winning strategy on a winnable Nim instance by internalizing the proof in LP of the formalized version of that instance.