IDEAS home Printed from https://ideas.repec.org/a/eee/mateco/v66y2016icp26-39.html
   My bibliography  Save this article

An introduction to mechanized reasoning

Author

Listed:
  • Kerber, Manfred
  • Lange, Christoph
  • Rowat, Colin

Abstract

Mechanized reasoning uses computers to verify proofs and to help discover new theorems. Computer scientists have applied mechanized reasoning to economic problems but–to date–this work has not yet been properly presented in economics journals. We introduce mechanized reasoning to economists in three ways. First, we introduce mechanized reasoning in general, describing both the techniques and their successful applications. Second, we explain how mechanized reasoning has been applied to economic problems, concentrating on the two domains that have attracted the most attention: social choice theory and auction theory. Finally, we present a detailed example of mechanized reasoning in practice by means of a proof of Vickrey’s familiar theorem on second-price auctions.

Suggested Citation

  • Kerber, Manfred & Lange, Christoph & Rowat, Colin, 2016. "An introduction to mechanized reasoning," Journal of Mathematical Economics, Elsevier, vol. 66(C), pages 26-39.
    • Handle: RePEc:eee:mateco:v:66:y:2016:i:c:p:26-39
    DOI: 10.1016/j.jmateco.2016.06.005
    as

    Download full text from publisher

    File URL: http://www.sciencedirect.com/science/article/pii/S0304406816300362
    Download Restriction: Full text for ScienceDirect subscribers only
    File URL: https://libkey.io/10.1016/j.jmateco.2016.06.005?utm_source=ideas
    LibKey link: if access is restricted and if your library uses this service, LibKey will redirect you to where you can use your library subscription to access this item
    ---><---

    As the access to this document is restricted, you may want to search for a different version of it.

    References listed on IDEAS

    as
    1. Marco B Caminati & Manfred Kerber & Christoph Lange & Colin Rowat, 2015. "Sound Auction Specification and Implementation," Discussion Papers 15-08, Department of Economics, University of Birmingham.
    2. 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.
    3. Soo Chew & Shigehiro Serizawa, 2007. "Characterizing the Vickrey combinatorial auction by induction," Economic Theory, Springer;Society for the Advancement of Economic Theory (SAET), vol. 33(2), pages 393-406, November.
    4. Mark Armstrong, 2000. "Optimal Multi-Object Auctions," The Review of Economic Studies, Review of Economic Studies Ltd, vol. 67(3), pages 455-481.
    5. Barbera, Salvador, 1983. "Strategy-Proofness and Pivotal Voters: A Direct Proof of the Gibbard-Satterthwaite Theorem," International Economic Review, Department of Economics, University of Pennsylvania and Osaka University Institute of Social and Economic Research Association, vol. 24(2), pages 413-417, June.
    6. , & ,, 2015. "Strategy-proofness and efficiency with non-quasi-linear preferences: a characterization of minimum price Walrasian rule," Theoretical Economics, Econometric Society, vol. 10(2), May.
    7. Miki Kato & Shinji Ohseto & Shohei Tamura, 2015. "Strategy-proofness versus symmetry in economies with an indivisible good and money," International Journal of Game Theory, Springer;Game Theory Society, vol. 44(1), pages 195-207, February.
    8. Tsuyoshi Adachi, 2014. "Equity and the Vickrey allocation rule on general preference domains," Social Choice and Welfare, Springer;The Society for Social Choice and Welfare, vol. 42(4), pages 813-830, April.
    9. Kotaro Suzumura, 2000. "Presidential Address: Welfare Economics Beyond Welfarist-Consequentialism," The Japanese Economic Review, Japanese Economic Association, vol. 51(1), pages 1-32, March.
    10. John William Hatfield & Paul R. Milgrom, 2005. "Matching with Contracts," American Economic Review, American Economic Association, vol. 95(4), pages 913-935, September.
    11. Reny, Philip J., 2001. "Arrow's theorem and the Gibbard-Satterthwaite theorem: a unified approach," Economics Letters, Elsevier, vol. 70(1), pages 99-105, January.
    12. Kannai, Yakar & Peleg, Bezalel, 1984. "A note on the extension of an order on a set to the power set," Journal of Economic Theory, Elsevier, vol. 32(1), pages 172-175, February.
    13. Armstrong, Mark & Rochet, Jean-Charles, 1999. "Multi-dimensional screening:: A user's guide," European Economic Review, Elsevier, vol. 43(4-6), pages 959-979, April.
    14. Eric Maskin, 2004. "The Unity of Auction Theory: Paul Milgrom's Masterclass," Economics Working Papers 0044, Institute for Advanced Study, School of Social Science.
    15. Orhan Ayg?n & Tayfun S?nmez, 2013. "Matching with Contracts: Comment," American Economic Review, American Economic Association, vol. 103(5), pages 2050-2051, August.
    16. Ritxar Arlegi, 2003. "A note on Bossert, Pattanaik and Xu's “Choice under complete uncertainty: axiomatic characterization of some decision rules”," Economic Theory, Springer;Society for the Advancement of Economic Theory (SAET), vol. 22(1), pages 219-225, August.
    17. 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.
    18. Prasanta K. Pattanaik & Yongsheng Xu & Walter Bossert, 2000. "Choice under complete uncertainty: axiomatic characterizations of some decision rules," Economic Theory, Springer;Society for the Advancement of Economic Theory (SAET), vol. 16(2), pages 295-312.
    19. 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.
    20. Barbera, Salvador & Pattanaik, Prasanta K., 1984. "Extending an order on a Set to the power set: Some remarks on Kannai and Peleg's approach," Journal of Economic Theory, Elsevier, vol. 32(1), pages 185-191, February.
    21. Blume, Lawrence & Easley, David & Kleinberg, Jon & Kleinberg, Robert & Tardos, Éva, 2015. "Introduction to computer science and economic theory," Journal of Economic Theory, Elsevier, vol. 156(C), pages 1-13.
    22. Tang, Pingzhong & Lin, Fangzhen, 2011. "Two equivalence results for two-person strict games," Games and Economic Behavior, Elsevier, vol. 71(2), pages 479-486, 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. Casey B. Mulligan, 2018. "Quantifier Elimination for Deduction in Econometrics," NBER Working Papers 24601, National Bureau of Economic Research, Inc.
    2. Marco B Caminati & Manfred Kerber & Christoph Lange & Colin Rowat, 2015. "Sound Auction Specification and Implementation," Discussion Papers 15-08, Department of Economics, University of Birmingham.
    3. Takemura, Ryo, 2020. "Economic reasoning with demand and supply graphs," Mathematical Social Sciences, Elsevier, vol. 103(C), pages 25-35.

    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. Arlegi, Ricardo, 2007. "Sequentially consistent rules of choice under complete uncertainty," Journal of Economic Theory, Elsevier, vol. 135(1), pages 131-143, July.
    2. Barbera, S. & Bossert, W. & Pattanaik, P.K., 2001. "Ranking Sets of Objects," Cahiers de recherche 2001-02, Centre interuniversitaire de recherche en économie quantitative, CIREQ.
    3. Miller, Michael K., 2009. "Social choice theory without Pareto: The pivotal voter approach," Mathematical Social Sciences, Elsevier, vol. 58(2), pages 251-255, September.
    4. Jorge Alcalde-Unzu & Ricardo Arlegi & Miguel Ballester, 2013. "Uncertainty with ordinal likelihood information," Social Choice and Welfare, Springer;The Society for Social Choice and Welfare, vol. 41(2), pages 397-425, July.
    5. Walter Bossert & Kotaro Suzumura, 2011. "Rationality, external norms, and the epistemic value of menus," Social Choice and Welfare, Springer;The Society for Social Choice and Welfare, vol. 37(4), pages 729-741, October.
    6. Vázquez, Carmen, 2014. "Ranking opportunity sets on the basis of similarities of preferences: A proposal," Mathematical Social Sciences, Elsevier, vol. 67(C), pages 23-26.
    7. 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.
    8. 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.
    9. Alan Krause, 2008. "Ranking opportunity sets in a simple intertemporal framework," Economic Theory, Springer;Society for the Advancement of Economic Theory (SAET), vol. 35(1), pages 147-154, April.
    10. BOSSERT, Walter & SLINKO, Arkadii, 2004. "Relative Uncertainty and Additively Representable Set Rankings," Cahiers de recherche 2004-13, Universite de Montreal, Departement de sciences economiques.
    11. Kazumura, Tomoya & Mishra, Debasis & Serizawa, Shigehiro, 2020. "Strategy-proof multi-object mechanism design: Ex-post revenue maximization with non-quasilinear preferences," Journal of Economic Theory, Elsevier, vol. 188(C).
    12. Ran Spiegler, 2001. "Inferring a linear ordering over a power set," Theory and Decision, Springer, vol. 51(1), pages 31-49, August.
    13. Tam'as Fleiner & Zsuzsanna Jank'o & Akihisa Tamura & Alexander Teytelboym, 2015. "Trading Networks with Bilateral Contracts," Papers 1510.01210, arXiv.org, revised May 2018.
    14. Ritxar Arlegi, 2001. "Rational Evaluation of Actions Under Complete Uncertainty," Documentos de Trabajo - Lan Gaiak Departamento de Economía - Universidad Pública de Navarra 0114, Departamento de Economía - Universidad Pública de Navarra.
    15. Cato, Susumu, 2018. "Incomplete decision-making and Arrow’s impossibility theorem," Mathematical Social Sciences, Elsevier, vol. 94(C), pages 58-64.
    16. Arlegi, Ritxar & Dimitrov, Dinko, 2016. "Power set extensions of dichotomous preferences," Mathematical Social Sciences, Elsevier, vol. 83(C), pages 20-29.
    17. Ballester, Miguel A. & de Miguel, Juan R. & Nieto, Jorge, 2004. "Set comparisons in a general domain: the Indirect Utility Criterion," Mathematical Social Sciences, Elsevier, vol. 48(2), pages 139-150, September.
    18. Chen, Peter & Egesdal, Michael & Pycia, Marek & Yenmez, M. Bumin, 2016. "Median stable matchings in two-sided markets," Games and Economic Behavior, Elsevier, vol. 97(C), pages 64-69.
    19. , & ,, 2015. "Strategy-proofness and efficiency with non-quasi-linear preferences: a characterization of minimum price Walrasian rule," Theoretical Economics, Econometric Society, vol. 10(2), May.
    20. Ehlers, Lars & Klaus, Bettina, 2016. "Object allocation via deferred-acceptance: Strategy-proofness and comparative statics," Games and Economic Behavior, Elsevier, vol. 97(C), pages 128-146.

    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:eee:mateco:v:66:y:2016:i:c:p:26-39. 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: Catherine Liu (email available below). General contact details of provider: http://www.elsevier.com/locate/jmateco .

    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.