Commit 5efa72a9 authored by Lawrence Paulson's avatar Lawrence Paulson
Browse files

new entry SDS_Impossibility

parent 007fb04238f4
......@@ -220,6 +220,7 @@ Ribbon_Proofs
Robbins-Conjecture
Roy_Floyd_Warshall
SATSolverVerification
SDS_Impossibility
SIFPL
SIFUM_Type_Systems
Secondary_Sylow
......
chapter AFP
session "SDS_Impossibility" (AFP) = "Randomised_Social_Choice" +
theories
SDS_Impossibility
document_files
"root.tex"
"root.bib"
This diff is collapsed.
# -*- shell-script -*-
# Get email when automated build fails. May be empty.
# values: "email1 email2 .. emailn"
NOTIFY="eberlm@in.tum.de"
# Participate in frequent (nightly) build (only for small submissions)
# values: "yes" "no"
FREQUENT="yes"
@article{extendrd,
title = "The impossibility of extending {R}andom {D}ictatorship to weak preferences",
journal = "Economics Letters",
volume = "141",
pages = "pp. 44 -- 47",
year = "2016",
issn = "0165-1765",
doi = "http://dx.doi.org/10.1016/j.econlet.2016.01.028",
url = "http://www.sciencedirect.com/science/article/pii/S0165176516300209",
author = "Florian Brandl and Felix Brandt and Warut Suksompong"
}
@article{smt,
title = "Proving the incompatibility of {E}fficiency and {S}trategyproofness via {SMT} solving",
author = "Florian Brandl and Felix Brandt and Christian Geist",
journal = "Proceedings of the 25th International Joint Conference on Artificial Intelligence (IJCAI)",
year = "2016",
note = "Forthcoming"
}
\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym}
% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed
%\usepackage{amssymb}
%for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
%\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
%\<triangleq>, \<yen>, \<lozenge>
%\usepackage{eurosym}
%for \<euro>
%\usepackage[only,bigsqcap]{stmaryrd}
%for \<Sqinter>
%\usepackage{eufrak}
%for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
%\usepackage{textcomp}
%for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
%\<currency>
% this should be the last package used
\usepackage{pdfsetup}
% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}
% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}
\begin{document}
\title{The Incompatibility of \textit{SD}-Efficiency and \textit{SD}-Strategy-Proofness}
\author{Manuel Eberl}
\maketitle
\begin{abstract}
This formalisation contains the proof that there is no anonymous and neutral Social Decision Scheme for at least four voters and alternatives that fulfils both \textit{SD}-Efficiency and \textit{SD}-Strategy-Proofness. The proof is a fully structured and quasi-human-redable one. It was derived from the (unstructured) SMT proof of the case for exactly four voters and alternatives by Brandl\ \textit{et~al.}~\cite{smt}.
Their proof relies on an unverified translation of the original problem to SMT, and the proof that lifts the argument for exactly four voters and alternatives to the general case is also not machine-checked.
In this Isabelle proof, on the other hand, all of these steps are also fully proven and machine-checked. This is particularly important seeing as a previously published informal proof of a weaker statement contained a mistake in precisely this lifting step.~\cite{extendrd}
\end{abstract}
\tableofcontents
\parindent 0pt\parskip 0.5ex
\newpage
\input{session}
\bibliographystyle{abbrv}
\bibliography{root}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
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