TheoryGuru: a Mathematica package to apply quantifier elimination technology to economics

DOI10.1007/978-3-319-96418-8_44zbMATH Open1395.68350arXiv1806.10925OpenAlexW3098714707MaRDI QIDQ1662274FDOQ1662274

Casey B. Mulligan, James H. Davenport, Matthew England

Publication date: 17 August 2018

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.

Full work available at URL: https://arxiv.org/abs/1806.10925

Recommendations

• Mathematica as an environment for doing economics and econometrics
• An introduction to mechanized reasoning
• scientific article; zbMATH DE number 432656
• Real quantifier elimination in the RegularChains library
• Quantifier elimination for real algebra -- the quadratic case and beyond

zbMATH Keywords

quantifier eliminationgender wage gapeconomic reasoning

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Software, source code, etc. for problems pertaining to game theory, economics, and finance (91-04)

Cited In (9)

• Explainable AI insights for symbolic computation: a case study on selecting the variable ordering for cylindrical algebraic decomposition
• Cylindrical algebraic decomposition with equational constraints
• A Machine Learning Based Software Pipeline to Pick the Variable Ordering for Algorithms with Polynomial Inputs
• Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
• Theoryguru
• Constrained neural networks for interpretable heuristic creation to optimise computer algebra systems
• Curtains in CAD: Why Are They a Problem and How Do We Fix Them?
• Improved Cross-Validation for Classifiers that Make Algorithmic Choices to Minimise Runtime Without Compromising Output Correctness
• Using Theorema in the Formalization of Theoretical Economics

Uses Software

• Mathematica

This page was built for publication: TheoryGuru: a Mathematica package to apply quantifier elimination technology to economics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1662274)