Skip to Main content Skip to Navigation
New interface
Preprints, Working Papers, ...

Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant

Abstract : Decision theory and game theory are both interdisciplinary domains that focus on modeling and studying decision-making processes. On the one hand, decision theory aims to account for the possible behaviors of an agent with respect to an uncertain situation. It thus provides several frameworks to describe the decision-making processes in this context, including that of belief functions. On the other hand, game theory focuses on multi-agent decisions, typically with probabilistic uncertainty (if any), hence the so-called class of Bayesian games. In this paper, we extend Bayesian games to the theory of belief functions. We obtain a more expressive class of games we refer to as Bel games; it make it possible to better capture human behaviors with respect to lack of information. Next, we prove an extended version of the so-called Howson-Rosenthal's theorem, showing that Bel games can be turned into games of complete information, i.e., without any uncertainty. Doing so, we embed this class of games into classical game theory and thereby enable the use of existing algorithms. Using the Coq proof assistant, we formalize a theory of belief functions, and formally verify three different proofs of Howson-Rosenthal's theorem.
Complete list of metadata
Contributor : Pierre POMERET-COQUOT Connect in order to contact the contributor
Submitted on : Wednesday, September 21, 2022 - 12:20:35 PM
Last modification on : Thursday, September 22, 2022 - 5:13:37 AM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License


  • HAL Id : hal-03782650, version 1


Pierre Pomeret-Coquot, Hélène Fargier, Érik Martin-Dorel. Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant. {date}. ⟨hal-03782650⟩



Record views


Files downloads