arXiv subjects

C. Mulligan

Publications and source records attributed to C. Mulligan.

2 recordsLinked to original sources

arXiv2018

Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics

We consider problems originating in economics that may be solved automatically using mathematical software. We present and make freely available a new benchmark set of such problems. The problems have been shown to fall within the framework of non-linear real arithmetic, and so are in theory soluble via Quantifier Elimination (QE) technology as usually implemented in computer algebra systems. Further, they all can be phrased in prenex normal form with only existential quantifiers and so are also admissible to those Satisfiability Module Theory (SMT) solvers that support the QF_NRA. There is a great body of work considering QE and SMT application in science and engineering, but we demonstrate here that there is potential for this technology also in the social sciences.

cs.SC↗

arXiv2018

TheoryGuru: A Mathematica Package to apply Quantifier Elimination

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.

cs.SC↗