Projects per year
Abstract
Novel auction schemes are constantly being designed. Their design has significant consequences for the allocation of goods and the revenues generated. But how to tell whether a new design has the desired properties, such as efficiency, i.e. allocating goods to those bidders who value them most? We say: by formal, machinechecked proofs. We investigated the suitability of the Isabelle, Theorema, Mizar, and Hets/CASL/TPTP theorem provers for reproducing a key result of auction theory: Vickrey’s 1961 theorem on the properties of secondprice auctions. Based on our formalisation experience, taking an auction designer’s perspective, we give recommendations on what system to use for formalising auctions, and outline further steps towards a complete auction theory toolbox.
Original language  English 

Title of host publication  Intelligent Computer Mathematics 
Editors  Jacques Carette, James Davenport, Wolfgang Windsteiger, Petr Sojka, David Aspinall, Christoph Lange 
Publisher  Springer 
Pages  200215 
Volume  7961 
ISBN (Electronic)  9783642393204 
ISBN (Print)  9783642393198 
DOIs  
Publication status  Published  2013 
Event  Conferences on Intelligent Computer Mathematics  Bath, United Kingdom Duration: 8 Jul 2013 → 12 Jul 2013 
Publication series
Name  Lecture Notes in Computer Science 

Publisher  Springer 
Volume  7961 
ISSN (Print)  03029743 
Conference
Conference  Conferences on Intelligent Computer Mathematics 

Country/Territory  United Kingdom 
City  Bath 
Period  8/07/13 → 12/07/13 
Projects
 1 Finished

Formal Representation and Proof for Cooperative Games: A Foundation for Complex Social Behaviour
Kerber, M. & Rowat, C.
ENGINEERING & PHYSICAL SCIENCE RESEARCH COUNCIL
1/05/12 → 30/04/15
Project: Research Councils