Coq和Isabelle中纳什均衡存在定理的形式化证明
计算机科学与博弈论
2017-09-08 v1 计算机科学中的逻辑
摘要
纳什均衡(NE)是博弈论中的一个核心概念。在这里，我们在两个证明助手Coq和Isabelle中正式证明了一个关于NE存在的已发表定理：从一个具有有限结果的博弈开始，可以通过将每个结果重写为两个基本结果之一（即玩家1获胜或玩家2获胜）来推导出一个博弈。如果所有推导这种赢/输博弈的方式都导致一个玩家拥有获胜策略的博弈，那么原始博弈也存在纳什均衡。本文还做出了另外三个贡献：首先，虽然原始证明调用了严格偏序的线性扩展，但这里我们通过推广相关定义来避免它。其次，我们注意到该定理也暗示了安全均衡的存在，这是为模型检验引入的NE的更强版本。第三，我们还注意到该定理的构造性证明在拟多项式时间内为非零和优先博弈（推广了奇偶博弈）计算安全均衡。
引用
@article{arxiv.1709.02096,
title = {An Existence Theorem of Nash Equilibrium in Coq and Isabelle},
author = {Stéphane Le Roux and Érik Martin-Dorel and Jan-Georg Smaus},
journal= {arXiv preprint arXiv:1709.02096},
year = {2017}
}
备注
In Proceedings GandALF 2017, arXiv:1709.01761