A Formal Proof of Vickrey's Theorem by Blast, Simp, and Rule

Manfred Kerber, Christoph Lange and Colin Rowat

Discussion Papers from Department of Economics, University of Birmingham

Abstract: Formal methods use computers to verify proofs or even discover new theorems. Interest in applying formal methods to problems in economics has increased in the past decade, but - to date - none of this work has been published in economics journals. This paper applies formal methods to a familiar environment - Vickrey's theorem on second-price auctions - and provides, as background, an introduction to formal methods.

Keywords: formal proof; mechanized reasoning; auction theory (search for similar items in EconPapers)
JEL-codes: B41 C63 C88 D44 (search for similar items in EconPapers)
Pages: 12 pages
Date: 2014-01
New Economics Papers: this item is included in nep-hpe
References: View references in EconPapers View complete reference list from CitEc
Citations: View citations in EconPapers (1)

Downloads: (external link)
https://repec.cal.bham.ac.uk/pdf/14-01.pdf

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:bir:birmec:14-01

Access Statistics for this paper

More papers in Discussion Papers from Department of Economics, University of Birmingham Contact information at EDIRC.
Bibliographic data for series maintained by Oleksandr Talavera ().