2026-07-24T03:16:09Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18400 2024-03-12T12:01:29Z ddc:004 open_access

Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant Pomeret-Coquot, Pierre Fargier, Hélène Martin-Dorel, Érik Game of Incomplete Information Belief Function Theory Coq Proof Assistant SSReflect Proof Language MathComp Library Decision theory and game theory are both interdisciplinary domains that focus on modelling and {analyzing} 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 use the Coq/SSReflect proof assistant to formally prove the results we obtained in [Pierre Pomeret{-}Coquot et al., 2022]. First, we formalize a general theory of belief functions with finite support, and structures and solutions concepts from game theory. On top of that, we extend Bayesian games to the theory of belief functions, so that we obtain a more expressive class of games we refer to as Bel games; it makes it possible to better capture human behaviors with respect to lack of information. Next, we provide three different proofs of an extended version of the so-called Howson-Rosenthal’s theorem, showing that Bel games can be casted into games of complete information, i.e., without any uncertainty. We thus embed this class of games into classical game theory, enabling the use of existing algorithms. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Pierre Pomeret-Coquot and Hélène Fargier and Érik Martin-Dorel 2023 Is Part Of LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2023.25 urn:nbn:de:0030-drops-184001 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.25 eng https://creativecommons.org/licenses/by/4.0/legalcode