An Existence Theorem of Nash Equilibrium in Coq and Isabelle
An Existence Theorem of Nash Equilibrium in Coq and Isabelle
复制标题
Coq和Isabelle纳什均衡的存在定理
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
J. Smaus
中科院分区：
文献类型：
--
作者：
Stéphane Le Roux;Érik Martin;J. Smaus
纳什均衡是博弈论中的一个核心概念。在这里，我们正式证明了一个已发表的定理存在一个NE在两个证明助理，Coq和Isabelle：从一个游戏开始，许多结果，一个可以得到一个游戏重写这些结果与两个基本结果之一，即玩家1获胜或玩家2获胜。如果所有的方式得出这样一个赢/输的游戏导致一个游戏，其中一个球员有一个胜利的战略，原来的游戏也有一个纳什均衡。这篇文章做了三个其他的贡献：第一，虽然原来的证明调用严格偏序的线性扩展，在这里我们通过推广相关的定义来避免它。其次，我们注意到该定理还意味着存在一个安全均衡，这是一个更强的NE版本，被引入用于模型检查。第三，我们还注意到，该定理的构造性证明在准多项式时间内计算非零和优先级游戏（广义奇偶游戏）的安全均衡。
Nash equilibrium (NE) is a central concept in game theory. Here we prove formally a published theorem on existence of an NE in two proof assistants, Coq and Isabelle: starting from a game with finitely many outcomes, one may derive a game by rewriting each of these outcomes with either of two basic outcomes, namely that Player 1 wins or that Player 2 wins. If all ways of deriving such a win/lose game lead to a game where one player has a winning strategy, the original game also has a Nash equilibrium. This article makes three other contributions: first, while the original proof invoked linear extension of strict partial orders, here we avoid it by generalizing the relevant definition. Second, we notice that the theorem also implies the existence of a secure equilibrium, a stronger version of NE that was introduced for model checking. Third, we also notice that the constructive proof of the theorem computes secure equilibria for non-zero-sum priority games (generalizing parity games) in quasi-polynomial time.