[isabelle] Two new AFP articles: "Social Choice Theory" and "Fun with Tilings"

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.

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 MHonArc.