Email Gateway (Aug 18 2022 at 12:38): Email Gateway (Aug 18 2022 at 12:38):From: Tobias Nipkow <nipkow@in.tum.de>
Some classical results in Social Choice Theory
Peter Gammie
Drawing on Sen's landmark work "Collective Choice and Social Welfare"
(1970), this development proves Arrow's General Possibility Theorem,
Sen's Liberal Paradox and May's Theorem in a general setting. The goal
was to make precise the classical statements and proofs of these
results, and to provide a foundation for more recent results such as the
Gibbard-Satterthwaite and Duggan-Schwartz theorems.
http://afp.sourceforge.net/entries/SenSocialChoice.shtml
Fun With Tilings
Tobias Nipkow and Lawrence Paulson
Tilings are defined inductively. It is shown that one form of mutilated
chess board cannot be tiled with dominoes, while another one can be
tiled with L-shaped tiles.
Please add further fun examples of this kind!
http://afp.sourceforge.net/devel-entries/FunWithTilings.shtml
Last updated: May 03 2024 at 04:19 UTC