Anzeige
Erschienen in:
2009 | OriginalPaper | Buchkapitel
Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence
verfasst von : Stéphane Le Roux
Erschienen in: Theorem Proving in Higher Order Logics
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
In a game from game theory, a Nash equilibrium (NE) is a combination of one strategy per agent such that no agent can increase its payoff by unilaterally changing its strategy. Kuhn proved that all (tree-like) sequential games have NE. Osborne and Rubinstein abstracted over these games and Kuhn’s result: they proved a sufficient condition on agents’
preferences
for all games to have NE. This paper proves a
necessary and sufficient condition
, thus accounting for the game-theoretic frameworks that were left aside.
The proof is formalised
using Coq, and contrary to usual game theory it adopts an inductive approach to trees for definitions and proofs. By rephrasing a few game-theoretic concepts, by ignoring useless ones, and by characterising the proof-theoretic strength of Kuhn’s/Osborne and Rubinstein’s development, this paper also
clarifies
sequential game theory. The introduction sketches these clarifications, while the rest of the paper details the formalisation.