A constructive approach to sequential Nash equilibria

We present a Coq-formalised proof that all non-cooperative, sequential games have a Nash equilibrium point. Our proof methodology follows the style advocated by LCFstyle 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 formalised game theory goes. Key words: Nash equilibria, automatic theorem proving, constructivity

• Type: Journal
• Year: 2006
• Where: IPL
• Authors: René Vestergaard
• Keywords: Coq-formalised Proof, IPL 2006, Nash Equilibrium Point, Simple Computational Means