An Existence Theorem of Nash Equilibrium in Coq and Isabelle

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...

Full description

Bibliographic Details
Main Authors: Stéphane Le Roux, Érik Martin-Dorel, Jan-Georg Smaus
Format: Article
Language:English
Published: Open Publishing Association 2017-09-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1709.02096v1