Update: The ITP2023 formalization is available on the ITP2023 branch.
We formalize several results from uncertainty theories, decision theories and game theories. The formalization offers some usable structures for set-functions (mass functions and capacities)
We also prove Howson and Rosenthal like transforms in a algebraic way and for generalized Bel-Games. They cast games of incomplete information to games of complete information so they can be studied with the classical game theoretic tools.
Note 1: The ITP formalization has moved on the ITP2023 branch.
Note 2: This extended formalization match my PhD thesis which will be linked when published.
- Author(s):
- Pierre Pomeret-Coquot (initial)
- Erik Martin-Dorel (initial)
- Hélène Fargier (initial)
- License: MIT
- Compatible Coq versions: 8.16 or later
- Additional dependencies:
- MathComp 2.0.0
- Coq namespace:
BelGames
- Related publication(s):
To build and install manually, do:
git clone https://github.com/pPomCo/belgames.git
cd belgames
make # or make -j <number-of-cores-on-your-machine>
make install