ForMaRE – Formal Mathematical Reasoning in Economics

ForMaRE applies formal mathematical reasoning to economics. It received funding by the EPSRC grant EP/J007498/1 (“Formal Representation and Proof for Cooperative Games: A Foundation for Complex Social Behaviour”).

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 computer science, we seek to present user experience feedback from new audiences, as well as new challenge problems, thus contributing to the development of formal methods.

For more details, we recommend this short project description, as well as our publications, our software (integrating specifications, executable code and theorems about the former), and news items in the archive.

Peopledetails about the people behind ForMaRE

At the University of Birmingham, ForMaRE is run by Manfred Kerber, Colin Rowat, Marco B. Caminati, and Christoph Lange.

We collaborate with a number of external international researchers, including computer scientists as well as economists.

Main research outputsfull publication list

  1. Problem set for first order theorem provers in the TPTP format (as part of the Auction Theory Toolbox (ATT))
  2. Marco B. Caminati, Manfred Kerber, Christoph Lange, Colin Rowat. VCG - Combinatorial Vickrey-Clarke-Groves Auctions . 2015-04-30, Archive of Formal Proofs. ISSN 2150-914x
  3. Marco B. Caminati, Manfred Kerber, Christoph Lange, Colin Rowat. Sound Auction Specification and Implementation . EC'15, 16th ACM Conference on Economics and Computation (slides by Colin Rowat at pubs/ec15-slides.pdf).
  4. Simon MacKenzie, Manfred Kerber, Colin Rowat. Pillage games with multiple stable sets. International Journal of Game Theory, electronic version March 2015, printed version November 2015, Volume 44, Issue 4, pp 993-1013.
  5. Colin Rowat, Manfred Kerber. Sufficient Conditions for Unique Stable Sets in Three Agent Pillage Games. Mathematical Social Sciences, vol 69, pp. 69 - 80, May 2014.
  6. Marco B. Caminati, Manfred Kerber, Christoph Lange, Colin Rowat. Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle?. Conference on Intelligent Computer Mathematics No. 8543 in Lecture Notes in Computer Science, Springer, pp. 236–251, 2014.
  7. Christoph Lange, Colin Rowat, Manfred Kerber. The ForMaRE Project – Formal Mathematical Reasoning in Economics. Conference on Intelligent Computer Mathematics (CICM, systems & projects track). No. 7961 in Lecture Notes in Computer Science, Springer, pp. 330–334, 2013. (Project description and first-year summary, from a formal methods perspective)
  8. Christoph Lange, Marco B. Caminati, Manfred Kerber, Till Mossakowski, Colin Rowat, Makarius Wenzel, Wolfgang Windsteiger. A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory. Conference on Intelligent Computer Mathematics (CICM, mathematical knowledge management track). No. 7961 in Lecture Notes in Computer Science, Springer, pp. 200–215, 2013. (accompanying formalisations evolve in the Auction Theory Toolbox)
  9. Christoph Lange, Colin Rowat, Manfred Kerber. Enabling Domain Experts to use Formalised Reasoning (Do-Form), symposium at the AISB Annual Convention, 2013. Edition of a special issue Enabling Domain Experts to Use Formalized Reasoning of the journal Mathematics in Computer Science
  10. Manfred Kerber, Christoph Lange, Colin Rowat. An economist's guide to mechanized reasoning or My computer just proved 84 impossibility theorems. Initiative for Computational Economics, 2012 (invited lecture). (Overview on the potential of applying formal methods to economics, from an economics perspective)

Internal

Internal information for the project members

This page was last modified on 18 February 2016.