An existence theorem of Nash equilibrium in Coq and Isabelle

MaRDI QIDQ3384162zbMATH OpenFDO

Authors Stéphane Le Roux, Érik Martin-Dorel, Jan-Georg Smaus

Publication date 14 December 2021

Full work available at URL https://arxiv.org/abs/1709.02096, http://eptcs.web.cse.unsw.edu.au/paper.cgi?GANDALF2017.4

Mathematics Subject Classification ID

Noncooperative games (91A10) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• A constructive approach to sequential Nash equilibria
• Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence
• A note on proofs of existence of Nash equilibria in finite strategic games, of two players
• Constructive proof of the existence of Nash equilibrium in a finite strategic game with sequentially locally nonconstant payoff functions
• From winning strategy to Nash equilibrium

Cites work

• scientific article; zbMATH DE number 4095249 (Why is no real title available?)
• A proof of the four color theorem
• Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence
• Borel determinacy
• Cores of effectivity functions and implementation theory
• Deciding parity games in quasipolynomial time
• Equilibria in quantitative reachability games
• Formal proof - the four color theorem
• From winning strategy to Nash equilibrium
• Games with secure equilibria
• Manipulation of Voting Schemes: A General Result
• The solvability of positional games in pure strategies
• ``Backward coinduction, Nash equilibrium and the rationality of escalation

Cited in

(4)

• A library for algorithmic game theory in \textsf{Ssreflect/Coq}
• A note on proofs of existence of Nash equilibria in finite strategic games, of two players
• Monotone bargaining is Nash-solvable
• scientific article; zbMATH DE number 7136658 (Why is no real title available?)

Describes a project that uses

Uses Software

• Isabelle
• Coq

This page was built for publication: An existence theorem of Nash equilibrium in Coq and Isabelle

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3384162)