Abstract
The ForMaRE project applies formal mathematical reasoning to economics. We seek to increase confidence in economics’ theoretical results, to aid in discovering new results, and to foster interest in formal methods, i.e. computer-aided reasoning, within economics. To formal methods, we seek to contribute user experience feedback from new audiences, as well as new challenge problems. In the first project year, we continued earlier game theory studies but then focused on auctions, where we are building a toolbox of formalisations, and have started to study matching and financial risk. In parallel to conducting research that connects economics and formal methods, we organise events and provide infrastructure to connect both communities, from fostering mutual awareness to targeted matchmaking. These efforts extend beyond economics, towards generally enabling domain experts to use mechanised reasoning.
This work has been supported by EPSRC grant EP/J007498/1.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Applicant auction for top-level domains, http://applicantauction.com
Formalising ‘100’ theorems/models/theories in economics, http://cs.bham.ac.uk/research/projects/formare/planetary/content/100-theorems
Geist, C., Endriss, U.: Automated search for impossibility theorems in social choice theory: ranking sets of objects. Artificial Intelligence Research 40 (2011)
Initiative for Computational Economics, http://ice.uchicago.edu
Kerber, M.: Automated Reasoning for Economics. Invited lecture at the Automated Reasoning Workshop (ARW) (2013)
Kerber, M., Rowat, C., Windsteiger, W.: Using Theorema in the Formalization of Theoretical Economics. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) Calculemus/MKM 2011. LNCS (LNAI), vol. 6824, pp. 58–73. Springer, Heidelberg (2011)
Kohlhase, M.: The Planetary Project: Towards eMath3.0. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS (LNAI), vol. 7362, pp. 448–452. Springer, Heidelberg (2012)
Lange, C., Kerber, M., Rowat, C.: Applying Mechanised Reasoning in Economics – Making Reasoners Applicable for Domain Experts. Tutorial at the annual meeting of the German Informatics Society (2013), http://cs.bham.ac.uk/research/projects/formare/events/informatik2013
Lange, C., Rowat, C., Kerber, M. (eds.): Enabling Domain Experts to use Formalised Reasoning. Symposium at the AISB Annual Convention (2013), http://cs.bham.ac.uk/research/projects/formare/events/aisb2013/
Lange, C., Caminati, M.B., Kerber, M., Mossakowski, T., Rowat, C., Wenzel, M., Windsteiger, W.: A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol. 7961, pp. 200–215. Springer, Heidelberg (2013); arXiv:1303.4193 [cs.LO]
Lange, C., et al.: Auction Theory Toolbox (2013), http://cs.bham.ac.uk/research/projects/formare/code/auction-theory/
Maskin, E.: The unity of auction theory: Milgrom’s master class. Economic Literature 42(4) (2004)
Nipkow, T.: Social choice theory in HOL: Arrow and Gibbard-Satterthwaite. Automated Reasoning 43(3) (2009)
Sönmez, T., Unver, M.U.: Matching, Allocation, and Exchange of Discrete Resources. In: Handbook of Social Economics, vol. 1A. North-Holland (2011)
Tang, P., Lin, F.: Discovering theorems in game theory: two-person games with unique pure Nash equilibrium payoffs. Artificial Intelligence 175(14-15) (2011)
Vosloo, N.: Model Validation and Test Portfolios in Financial Regulation. In: Enabling Domain Experts to use Formalised Reasoning. AISB (2013)
Wiedijk, F.: Formalizing 100 Theorems, http://cs.ru.nl/~freek/100/
Wiedijk, F.: Formalizing Arrow’s theorem. Sādhanā 34(1) (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lange, C., Rowat, C., Kerber, M. (2013). The ForMaRE Project – Formal Mathematical Reasoning in Economics. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds) Intelligent Computer Mathematics. CICM 2013. Lecture Notes in Computer Science(), vol 7961. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39320-4_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-39320-4_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39319-8
Online ISBN: 978-3-642-39320-4
eBook Packages: Computer ScienceComputer Science (R0)