Propositional Games with Explicit Strategies
Bryan Renne · Electronic Notes in Theoretical Computer Science · 2006
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.