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

Casey Mulligan, Russell Bradford, James H. Davenport, Matthew England, Zak Tonks

Research output: Chapter in Book/Report/Conference proceedingConference proceeding

7 Citations (Scopus)
12 Downloads (Pure)

Abstract

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.
Original languageEnglish
Title of host publicationProceedings of the 3rd International Workshop on Satisfiability Checking and Symbolic Computation
EditorsAnna M Bigatti, Martin Brain
PublisherCEUR Workshop Proceedings
Number of pages13
Publication statusPublished - 1 Sep 2018
EventThird International Workshop on Satisfiability Checking and Symbolic Computation 2018 - Oxford, United Kingdom
Duration: 7 Jul 20189 Jul 2018
Conference number: 3

Conference

ConferenceThird International Workshop on Satisfiability Checking and Symbolic Computation 2018
Abbreviated titleSC 2018
CountryUnited Kingdom
CityOxford
Period7/07/189/07/18

Bibliographical note

Copyright © 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.

Fingerprint Dive into the research topics of 'Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics'. Together they form a unique fingerprint.

  • Cite this

    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.