Advertisement

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)

Abstract

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.

Keywords

Quantifier elimination Economic reasoning 

References

  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). https://doi.org/10.1145/3087604.3087622
  2. 2.
    Caviness, B., Johnson, J.: Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts & Monographs in Symbolic Computation. Springer, Wien (1998).  https://doi.org/10.1007/978-3-7091-9459-1CrossRefzbMATHGoogle 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).  https://doi.org/10.1007/s00419-017-1271-8CrossRefGoogle 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).  https://doi.org/10.1007/3-540-07407-4_17. (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).  https://doi.org/10.1016/j.jsc.2015.11.010MathSciNetCrossRefzbMATHGoogle 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).  https://doi.org/10.1007/978-3-319-08434-3_8CrossRefGoogle Scholar
  7. 7.
    Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View. Springer, New York (2013).  https://doi.org/10.1007/978-3-540-74105-3CrossRefzbMATHGoogle 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).  https://doi.org/10.1016/j.jmateco.2014.08.007MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Mulligan, C.: Automated Economic Reasoning with Quantifier Elimination. NBER Working Paper No. 22922 (2016). https://doi.org/10.3386/w22922
  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: https://arxiv.org/abs/1806.11447
  11. 11.
    Mulligan, C., Rubinstein, Y.: Selection, investment, and women’s relative wages over time. Q. J. Econ. 123(3), 1061–1110 (2008).  https://doi.org/10.1162/qjec.2008.123.3.1061CrossRefGoogle 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).  https://doi.org/10.1007/978-3-540-76591-2_11CrossRefGoogle Scholar
  13. 13.
    Strzeboński, A.: Cylindrical algebraic decomposition using validated numerics. J. Symbolic Comput. 41(9), 1021–1038 (2006).  https://doi.org/10.1016/j.jsc.2006.06.004MathSciNetCrossRefzbMATHGoogle 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). https://doi.org/10.1145/1837934.1837952
  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). https://doi.org/10.1145/2442829.2442877
  16. 16.
    Strzeboński, A.: Cylindrical algebraic decomposition using local projections. J. Symbolic Comput. 76, 36–64 (2016).  https://doi.org/10.1016/j.jsc.2015.11.018MathSciNetCrossRefzbMATHGoogle 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).  https://doi.org/10.1016/S0747-7171(88)80003-8MathSciNetCrossRefzbMATHGoogle 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