What Theorem Prover to use for Verifying Auctions?

Add to your list(s) Download to your calendar using vCal

• Christoph Lange (University of Birmingham, School of Computer Science)
• Wednesday 03 July 2013, 13:00-14:00
• UG06, Learning Centre.

If you have a question about this talk, please contact Christine Zarges.

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, machine-checked 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 second-price 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.

This talk is part of the Computer Science Lunch Time Talk Series series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Computer Science Lunch Time Talk Series
• UG06, Learning Centre
• computer sience

Note that ex-directory lists are not shown.