Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Randomised Social Choice


view this post on Zulip Email Gateway (Aug 22 2022 at 13:18):

From: Lawrence Paulson <lp15@cam.ac.uk>
Material is coming in quick and fast. Here is a new entry on Social Choice Theory. Many thanks, Manuel!

Larry Paulson

Randomised Social Choice Theory
Manuel Eberl

This work contains a formalisation of basic Randomised Social Choice, including Stochastic Dominance and Social Decision Schemes (SDSs) along with some of their most important properties (Anonymity, Neutrality, ex-post- and SD-Efficiency, SD-Strategy-Proofness) and two particular SDSs – Random Dictatorship and Random Serial Dictatorship (with proofs of the properties that they satisfy). Many important properties of these concepts are also proven – such as the two equivalent characterisations of Stochastic Dominance and the fact that SD-efficiency of a lottery only depends on the support. The entry also provides convenient commands to define Preference Profiles, prove their well-formedness, and automatically derive restrictions that sufficiently nice SDSs need to satisfy on the defined profiles. Currently, the formalisation focuses on weak preferences and Stochastic Dominance, but it should be easy to extend it to other domains – such as strict preferences – or other lottery extensions – such as Bilinear Dominance or Pairwise Comparison.

http://www.isa-afp.org/entries/Randomised_Social_Choice.shtml


Last updated: Nov 21 2024 at 12:39 UTC