A constructive approach to sequential Nash equilibria |
| |
Authors: | René Vestergaard |
| |
Affiliation: | School of Information Science, JAIST, Nomi, Ishikawa 923-1292, Japan |
| |
Abstract: | We present a Coq-formalized proof that all non-cooperative, sequential games have a Nash equilibrium point. Our proof methodology follows the style advocated by LCF-style theorem provers, i.e., it is based on inductive definitions and is computational in nature. The proof (i) uses simple computational means, only, (ii) basically is by construction, and (iii) reaches a constructively stronger conclusion than informal efforts. We believe the development is a first as far as formalized game theory goes. |
| |
Keywords: | Nash equilibria Automatic theorem proving Constructivity |
本文献已被 ScienceDirect 等数据库收录! |
|