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 proceedingpeer-review

    40 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 Sept 2018
    EventThird International Workshop on Satisfiability Checking and Symbolic Computation 2018 - University of Oxford, Oxford, United Kingdom
    Duration: 7 Jul 20189 Jul 2018
    Conference number: 3
    http://www.sc-square.org/CSA/workshop3.html

    Conference

    ConferenceThird International Workshop on Satisfiability Checking and Symbolic Computation 2018
    Abbreviated titleSC 2018
    Country/TerritoryUnited Kingdom
    CityOxford
    Period7/07/189/07/18
    Internet address

    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