An introduction to mechanized reasoning

Manfred Kerber, Christoph Lange and Colin Rowat

Journal of Mathematical Economics, 2016, vol. 66, issue C, 26-39

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.

Keywords: Mechanized reasoning; Formal methods; Social choice theory; Auction theory (search for similar items in EconPapers)
Date: 2016
References: View references in EconPapers View complete reference list from CitEc
Citations: View citations in EconPapers (3)

Downloads: (external link)
http://www.sciencedirect.com/science/article/pii/S0304406816300362
Full text for ScienceDirect subscribers only

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:eee:mateco:v:66:y:2016:i:c:p:26-39

DOI: 10.1016/j.jmateco.2016.06.005

Access Statistics for this article

Journal of Mathematical Economics is currently edited by Atsushi (A.) Kajii

More articles in Journal of Mathematical Economics from Elsevier
Bibliographic data for series maintained by Catherine Liu ().