Commit 2b9670c1 authored by Lawrence Paulson's avatar Lawrence Paulson
Browse files

Randomised_Social_Choice webpage

parent c8258bf12a6f
......@@ -875,7 +875,7 @@ title = A formalisation of the Cocke-Younger-Kasami algorithm
author = Maksym Bortin <mailto:Maksym.Bortin@nicta.com.au>
date = 2016-04-27
topic = Computer Science/Algorithms, Computer Science/Automata and Formal Languages
abstract =
abstract =
The theory provides a formalisation of the Cocke-Younger-Kasami
algorithm (CYK for short), an approach to solving the word problem
for context-free languages. CYK decides if a word is in the
......@@ -3640,7 +3640,7 @@ title = No Faster-Than-Light Observers
author = Mike Stannett <mailto:m.stannett@sheffield.ac.uk>, István Németi <http://www.renyi.hu/~nemeti/>
date = 2016-04-28
topic = Mathematics/Physics
abstract =
abstract =
We provide a formal proof within First Order Relativity Theory that no
observer can travel faster than the speed of light. Originally
reported in Stannett & Németi (2014) "Using Isabelle/HOL to verify
......@@ -3652,7 +3652,7 @@ title = Gröbner Bases Theory
author = Fabian Immler <http://www.in.tum.de/~immler/>, Alexander Maletzky <http://www.risc.jku.at/home/amaletzk>
date = 2016-05-02
topic = Mathematics/Algebra, Computer Science/Algorithms
abstract =
abstract =
This formalization is concerned with the theory of Gröbner bases in
(commutative) multivariate polynomial rings over fields, originally
developed by Buchberger in his 1965 PhD thesis. Apart from the
......@@ -3682,3 +3682,26 @@ abstract =
related to the overall argument. To obtain this structure, this entry uses set
monad notation for the set construction's definition, introduces suitable
predicates and rules, and follows a repeating structure in its Isar proof.
[Randomised_Social_Choice]
title = Randomised Social Choice Theory
author = Manuel Eberl <eberlm@in.tum.de>
date = 2016-05-05
topic = Mathematics/Economics
abstract =
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.
<!DOCTYPE public "-//w3c//dtd html 4.01 transitional//en"
"http://www.w3.org/TR/html4/loose.dtd">
<html>
<head>
<title>Archive of Formal Proofs</title>
<link rel="stylesheet" type="text/css" href="../front.css">
<script src="../jquery.min.js"></script>
<script src="../script.js"></script>
<link rel="icon" href="../images/favicon.ico" type="image/icon">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
<table width="100%">
<tbody>
<tr>
<td width="20%" align="center" valign="top">
<!-- navigation -->
<!--#include file="nav.html"-->
</td>
<td width="80%" valign="top">
<!-- content -->
<div align="center">
<p>&nbsp;</p>
<h1><font class="first">R</font>andomised
<font class="first">S</font>ocial
<font class="first">C</font>hoice
<font class="first">T</font>heory
</h1>
<p></p>
<table width="80%" class="data">
<tbody>
<tr><td class="datahead" width="20%">Title:</td>
<td class="data" width="80%">Randomised Social Choice Theory</td></tr>
<tr><td class="datahead">Author:</td>
<td class="data"><a href="eberlm@in.tum.de">Manuel Eberl</a></td></tr>
<tr><td class="datahead">Submission date:</td>
<td class="data">2016-05-05</td></tr>
<tr><td class="datahead" valign="top">Abstract:</td>
<td class="abstract">
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.
</td></tr>
<tr><td class="datahead" valign="top">BibTeX:</td>
<td class="formatted">
<pre>@article{Randomised_Social_Choice-AFP,
author = {Manuel Eberl},
title = {Randomised Social Choice Theory},
journal = {Archive of Formal Proofs},
month = may,
year = 2016,
note = {\url{http://isa-afp.org/entries/Randomised_Social_Choice.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="List-Index.shtml">List-Index</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
<!---INCLUDE- file="devel-warning.shtml"-->
</tbody>
</table>
<p></p>
<!--#set var="name" value="Randomised_Social_Choice" -->
<!--#set var="binfo" value="../browser_info/current/AFP/${name}" -->
<!--#set var="doc" value="${binfo}/document.pdf" -->
<!--#set var="outline" value="${binfo}/outline.pdf" -->
<!--#set var="browse" value="${binfo}/index.html" -->
<!--#set var="tar" value="../release/afp-${name}-current.tar.gz" -->
<table class="links">
<tbody>
<tr>
<td class="links">
<a href="<!--#echo var="outline" -->">Proof outline</a><br>
<a href="<!--#echo var="doc" -->">Proof document</a>
</td>
<!-- link to README.hmtl if no document exists -->
</tr>
<tr>
<td class="links">
<a href="<!--#echo var="browse" -->">Browse theories</a>
</td></tr>
<tr>
<td class="links">
<a href="<!--#echo var="tar" -->">Download this entry</a>
</td>
</tr>
<tr><td class="links">Older releases:
None </td></tr>
</tbody>
</table>
<!-- entry data end -->
</td> </tr> </table>
</body>
</html>
......@@ -49,6 +49,13 @@ A <a href="devel.shtml">development version</a> of the archive is available as w
<td class="head">2016</td>
</tr>
<tr><td class="entry">
2016-05-05:
<a href="entries/Randomised_Social_Choice.shtml">Randomised Social Choice Theory</a>
<br>Author:
<a href="eberlm@in.tum.de">Manuel Eberl</a>
</td></tr>
<tr><td class="entry">
2016-05-04:
<a href="entries/Bell_Numbers_Spivey.shtml">Spivey's Generalized Recurrence for Bell Numbers</a>
......
......@@ -398,6 +398,7 @@
<a href="entries/ArrowImpossibilityGS.shtml">ArrowImpossibilityGS</a> &nbsp;
<a href="entries/SenSocialChoice.shtml">SenSocialChoice</a> &nbsp;
<a href="entries/Vickrey_Clarke_Groves.shtml">Vickrey_Clarke_Groves</a> &nbsp;
<a href="entries/Randomised_Social_Choice.shtml">Randomised_Social_Choice</a> &nbsp;
</div>
<h3>Geometry</h3>
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment