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.
|Title of host publication||Proceedings of the 3rd International Workshop on Satisfiability Checking and Symbolic Computation|
|Editors||Anna M Bigatti, Martin Brain|
|Publisher||CEUR Workshop Proceedings|
|Number of pages||13|
|Publication status||Published - 1 Sep 2018|
|Event||Third International Workshop on Satisfiability Checking and Symbolic Computation 2018 - Oxford, United Kingdom|
Duration: 7 Jul 2018 → 9 Jul 2018
Conference number: 3
|Conference||Third International Workshop on Satisfiability Checking and Symbolic Computation 2018|
|Abbreviated title||SC 2018|
|Period||7/07/18 → 9/07/18|
Bibliographical noteCopyright © and Moral Rights are retained by the author(s) and/ or other copyright owners. A copy can be downloaded for personal non-commercial research or study, without prior permission or charge. This item cannot be reproduced or quoted extensively from without first obtaining permission in writing from the copyright holder(s). The content must not be changed in any way or sold commercially in any format or medium without the formal permission of the copyright holders.
Mulligan, C., Bradford, R., Davenport, J. H., England, M., & Tonks, Z. (2018). Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics. In A. M. Bigatti, & M. Brain (Eds.), Proceedings of the 3rd International Workshop on Satisfiability Checking and Symbolic Computation CEUR Workshop Proceedings.