TheoryGuru: A Mathematica Package to Apply Quantifier Elimination Technology to Economics

  • Casey B. MulliganEmail author
  • James H. Davenport
  • Matthew England
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10931)


We consider the use of Quantifier Elimination (QE) technology for automated reasoning in economics. There is a great body of work considering QE applications in science and engineering but we demonstrate here that it also has use in the social sciences. We explain how many suggested theorems in economics could either be proven, or even have their hypotheses shown to be inconsistent, automatically via QE.

However, economists who this technology could benefit are usually unfamiliar with QE, and the use of mathematical software generally. This motivated the development of a Mathematica Package TheoryGuru, whose purpose is to lower the costs of applying QE to economics. We describe the package’s functionality and give examples of its use.


Quantifier elimination Economic reasoning 


  1. 1.
    Bradford, R., Davenport, J., England, M., Errami, H., Gerdt, V., Grigoriev, D., Hoyt, C., Košta, M., Radulescu, O., Sturm, T., Weber, A.: A case study on the parametric occurrence of multiple steady states. In: Proceedings of the ISSAC 2017, pp. 45–52. ACM (2017).
  2. 2.
    Caviness, B., Johnson, J.: Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts & Monographs in Symbolic Computation. Springer, Wien (1998). Scholar
  3. 3.
    Charalampakis, A., Chatzigiannelis, I.: Analytical solutions for the minimum weight design of trusses by cylindrical algebraic decomposition. Arch. Appl. Mech. 88(1), 39–49 (2018). Scholar
  4. 4.
    Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975). (reprinted in [2])CrossRefGoogle Scholar
  5. 5.
    Erascu, M., Hong, H.: Real quantifier elimination for the synthesis of optimal numerical algorithms (Case study: square root computation). J. Symbolic Comput. 75, 110–126 (2016). Scholar
  6. 6.
    Huang, Z., et al.: Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 92–107. Springer, Cham (2014). Scholar
  7. 7.
    Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View. Springer, New York (2013). Scholar
  8. 8.
    Li, X., Wang, D.: Computing equilibria of semi-algebraic economies using triangular decomposition and real solution classification. J. Math. Econ. 54, 48–58 (2014). Scholar
  9. 9.
    Mulligan, C.: Automated Economic Reasoning with Quantifier Elimination. NBER Working Paper No. 22922 (2016).
  10. 10.
    Mulligan, C., Bradford, R., Davenport, J.H., England, M., Tonks, Z.: Non-linear real arithmetic benchmarks derived from automated reasoning in economics. In: Proceedings of the 3rd International Workshop on Satisfiability Checking and Symbolic Computation (\({\sf SC}^2\)) (2018, to appear). Preprint:
  11. 11.
    Mulligan, C., Rubinstein, Y.: Selection, investment, and women’s relative wages over time. Q. J. Econ. 123(3), 1061–1110 (2008). Scholar
  12. 12.
    Steinhorn, C.: Tame topology and O-minimal structures. In: Brown, D., Kubler, F. (eds.) Computational Aspects of General Equilibrium Theory, pp. 165–191. Springer, Heidelberg (2008). Scholar
  13. 13.
    Strzeboński, A.: Cylindrical algebraic decomposition using validated numerics. J. Symbolic Comput. 41(9), 1021–1038 (2006). Scholar
  14. 14.
    Strzeboński, A.: Computation with semialgebraic sets represented by cylindrical algebraic formulas. In: Proceedings of the ISSAC 2010, pp. 61–68. ACM (2010).
  15. 15.
    Strzeboński, A.: Solving polynomial systems over semialgebraic sets represented by cylindrical algebraic formulas. In: Proceedings of the ISSAC 2012, pp. 335–342. ACM (2012).
  16. 16.
    Strzeboński, A.: Cylindrical algebraic decomposition using local projections. J. Symbolic Comput. 76, 36–64 (2016). Scholar
  17. 17.
    Tarski, A.: A Decision Method For Elementary Algebra And Geometry. RAND Corporation, Santa Monica (1948). (reprinted in [2])zbMATHGoogle Scholar
  18. 18.
    Weispfenning, V.: The complexity of linear problems in fields. J. Symbolic Comput. 5(1/2), 3–27 (1988). Scholar
  19. 19.
    Wolfram, S.: The Mathematica Book. Wolfram Research Inc., San Francisco (2000)zbMATHGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Casey B. Mulligan
    • 1
    Email author
  • James H. Davenport
    • 2
  • Matthew England
    • 3
  1. 1.University of ChicagoChicagoUSA
  2. 2.University of BathBathUK
  3. 3.Coventry UniversityCoventryUK

Personalised recommendations