Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Two new AFP articles: "Social Choice Theory" a...


view this post on Zulip 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: Nov 21 2024 at 12:39 UTC