[isabelle] Two new AFP articles: "Social Choice Theory" and "Fun with Tilings"
- To: Mailing List Isabelle <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] Two new AFP articles: "Social Choice Theory" and "Fun with Tilings"
- From: Tobias Nipkow <nipkow at in.tum.de>
- Date: Mon, 17 Nov 2008 16:43:11 +0100
- User-agent: Thunderbird 220.127.116.11 (X11/20060909)
Some classical results in Social Choice Theory
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.
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!
This archive was generated by a fusion of
Pipermail (Mailman edition) and