IDEAS home Printed from https://ideas.repec.org/p/bir/birmec/14-01.html
   My bibliography  Save this paper

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

Author

Listed:
  • Manfred Kerber
  • Christoph Lange
  • Colin Rowat

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.

Suggested Citation

  • Manfred Kerber & Christoph Lange & Colin Rowat, 2014. "A Formal Proof of Vickrey's Theorem by Blast, Simp, and Rule," Discussion Papers 14-01, Department of Economics, University of Birmingham.
    • Handle: RePEc:bir:birmec:14-01
    as

    Download full text from publisher

    File URL: https://repec.cal.bham.ac.uk/pdf/14-01.pdf
    Download Restriction: no
    ---><---

    References listed on IDEAS

    as
    1. John Geanakoplos, 2005. "Three brief proofs of Arrow’s Impossibility Theorem," Economic Theory, Springer;Society for the Advancement of Economic Theory (SAET), vol. 26(1), pages 211-215, July.
    2. Milgrom,Paul, 2004. "Putting Auction Theory to Work," Cambridge Books, Cambridge University Press, number 9780521536721.
    3. Eric Maskin, 2004. "The Unity of Auction Theory: Milgrom's Masterclass," Journal of Economic Literature, American Economic Association, vol. 42(4), pages 1102-1115, December.
    4. Kotaro Suzumura, 2000. "Presidential Address: Welfare Economics Beyond Welfarist-Consequentialism," The Japanese Economic Review, Japanese Economic Association, vol. 51(1), pages 1-32, March.
    Full references (including those not matched with items on IDEAS)

    Citations

    Citations are extracted by the CitEc Project, subscribe to its RSS feed for this item.
    as


    Cited by:

    1. Kerber, Manfred & Lange, Christoph & Rowat, Colin, 2016. "An introduction to mechanized reasoning," Journal of Mathematical Economics, Elsevier, vol. 66(C), pages 26-39.

    Most related items

    These are the items that most often cite the same works as this one and are cited by the same works as this one.
    1. Kerber, Manfred & Lange, Christoph & Rowat, Colin, 2016. "An introduction to mechanized reasoning," Journal of Mathematical Economics, Elsevier, vol. 66(C), pages 26-39.
    2. Susumu Cato, 2013. "Alternative proofs of Arrow’s general possibility theorem," Economic Theory Bulletin, Springer;Society for the Advancement of Economic Theory (SAET), vol. 1(2), pages 131-137, November.
    3. Cato, Susumu, 2018. "Incomplete decision-making and Arrow’s impossibility theorem," Mathematical Social Sciences, Elsevier, vol. 94(C), pages 58-64.
    4. Laurent Lamy, 2013. "“Upping the ante”: how to design efficient auctions with entry?," RAND Journal of Economics, RAND Corporation, vol. 44(2), pages 194-214, June.
    5. Scott Duke Kominers & Alexander Teytelboym & Vincent P Crawford, 2017. "An invitation to market design," Oxford Review of Economic Policy, Oxford University Press and Oxford Review of Economic Policy Limited, vol. 33(4), pages 541-571.
    6. Amadou Boly & Robert Gillanders & Topi Miettinen, 2016. "Deterrence, peer effect, and legitimacy in anti-corruption policy-making: An experimental analysis," WIDER Working Paper Series 137, World Institute for Development Economic Research (UNU-WIDER).
    7. Jeremy Bulow & Jonathan Levin & Paul Milgrom, 2009. "Winning Play in Spectrum Auctions," NBER Working Papers 14765, National Bureau of Economic Research, Inc.
    8. Brunner, Christoph & Hu, Audrey & Oechssler, Jörg, 2014. "Premium auctions and risk preferences: An experimental study," Games and Economic Behavior, Elsevier, vol. 87(C), pages 467-484.
    9. Frank Kelly & Peter Key & Neil Walton, 2016. "Efficient Advert Assignment," Operations Research, INFORMS, vol. 64(4), pages 822-837, August.
    10. Sylvain Mignot & Stéphanie Saba & Annick Vignes, 2016. "To trust or to bid: an empirical analysis of social relationships on a fish market," Working Papers halshs-01298872, HAL.
    11. Lamprirni Zarpala & Dimitris Voliotis, 2022. "A core-selecting auction for portfolio's packages," Papers 2206.11516, arXiv.org, revised Feb 2024.
    12. Michael Padilla & Benjamin Van Roy, 2012. "Intermediated Blind Portfolio Auctions," Management Science, INFORMS, vol. 58(9), pages 1747-1760, September.
    13. Yokote, Koji, 2021. "Consistency of the doctor-optimal equilibrium price vector in job-matching markets," Journal of Economic Theory, Elsevier, vol. 197(C).
    14. Loertscher, Simon & Mezzetti, Claudio, 2021. "A dominant strategy, double clock auction with estimation-based tatonnement," Theoretical Economics, Econometric Society, vol. 16(3), July.
    15. Malueg, David A. & Orzach, Ram, 2009. "Revenue comparison in common-value auctions: Two examples," Economics Letters, Elsevier, vol. 105(2), pages 177-180, November.
    16. Alessandra Casella & Adam B. Cox, 2018. "A Property Rights Approach to Temporary Work Visas," The Journal of Legal Studies, University of Chicago Press, vol. 47(S1), pages 195-227.
    17. Nicolas C. Bedard & Jacob K. Goeree & Philippos Louis & Jingjing Zhang, 2020. "The Favored but Flawed Simultaneous Multiple-Round Auction," Working Paper Series 2020/03, Economics Discipline Group, UTS Business School, University of Technology, Sydney.
    18. Robert Kleinberg & Bo Waggoner & E. Glen Weyl, 2016. "Descending Price Optimally Coordinates Search," Papers 1603.07682, arXiv.org, revised Dec 2016.
    19. Steven Schilizzi & Uwe Latacz-Lohmann, 2012. "Evaluating Conservation Auctions with Unknown Bidder Costs: The Scottish Fishing Vessel Decommissioning Program," Land Economics, University of Wisconsin Press, vol. 88(4), pages 658-673.
    20. Hu, Audrey & Offerman, Theo & Zou, Liang, 2011. "Premium auctions and risk preferences," Journal of Economic Theory, Elsevier, vol. 146(6), pages 2420-2439.

    More about this item

    Keywords

    formal proof; mechanized reasoning; auction theory;
    All these keywords.

    JEL classification:

    • B41 - Schools of Economic Thought and Methodology - - Economic Methodology - - - Economic Methodology
    • C63 - Mathematical and Quantitative Methods - - Mathematical Methods; Programming Models; Mathematical and Simulation Modeling - - - Computational Techniques
    • C88 - Mathematical and Quantitative Methods - - Data Collection and Data Estimation Methodology; Computer Programs - - - Other Computer Software
    • D44 - Microeconomics - - Market Structure, Pricing, and Design - - - Auctions

    NEP fields

    This paper has been announced in the following NEP Reports:

    Statistics

    Access and download statistics

    Corrections

    All material on this site has been provided by the respective publishers and authors. You can help correct errors and omissions. When requesting a correction, please mention this item's handle: RePEc:bir:birmec:14-01. See general information about how to correct material in RePEc.

    If you have authored this item and are not yet registered with RePEc, we encourage you to do it here. This allows to link your profile to this item. It also allows you to accept potential citations to this item that we are uncertain about.

    If CitEc recognized a bibliographic reference but did not link an item in RePEc to it, you can help with this form .

    If you know of missing items citing this one, you can help us creating those links by adding the relevant references in the same way as above, for each refering item. If you are a registered author of this item, you may also want to check the "citations" tab in your RePEc Author Service profile, as there may be some citations waiting for confirmation.

    For technical questions regarding this item, or to correct its authors, title, abstract, bibliographic or download information, contact: Oleksandr Talavera (email available below). General contact details of provider: https://edirc.repec.org/data/debhauk.html .

    Please note that corrections may take a couple of weeks to filter through the various RePEc services.

    IDEAS is a RePEc service. RePEc uses bibliographic data supplied by the respective publishers.