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

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

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

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

University of Chicago
University of Bath

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding › peer-review

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

Conference

Conference	Third International Workshop on Satisfiability Checking and Symbolic Computation 2018
Abbreviated title	SC 2018
Country/Territory	United Kingdom
City	Oxford
Period	7/07/18 → 9/07/18
Internet address	http://www.sc-square.org/CSA/workshop3.html

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.

Access to Document

Post-printAccepted author manuscript, 628 KBLicence: CC BY

http://ceur-ws.org/Vol-2189/

Cite this

Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics. / Mulligan, Casey; Bradford, Russell; Davenport, James H. et al.
Proceedings of the 3rd International Workshop on Satisfiability Checking and Symbolic Computation. ed. / Anna M Bigatti; Martin Brain. CEUR Workshop Proceedings, 2018.

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding › peer-review

Mulligan, C, Bradford, R, Davenport, JH, England, M & Tonks, Z 2018, Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics. in AM Bigatti & M Brain (eds), Proceedings of the 3rd International Workshop on Satisfiability Checking and Symbolic Computation. CEUR Workshop Proceedings, Third International Workshop on Satisfiability Checking and Symbolic Computation 2018, Oxford, United Kingdom, 7/07/18. <http://ceur-ws.org/Vol-2189/>

@inproceedings{b83d2b3e3ab747f1beda425fd695591a,

title = "Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics",

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.",

author = "Casey Mulligan and Russell Bradford and Davenport, \{James H.\} and Matthew England and Zak Tonks",

note = "Copyright {\textcopyright} 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. ; Third International Workshop on Satisfiability Checking and Symbolic Computation 2018, SC 2018 ; Conference date: 07-07-2018 Through 09-07-2018",

year = "2018",

month = sep,

day = "1",

language = "English",

editor = "\{ Bigatti\}, \{Anna M \} and Brain, \{Martin \}",

booktitle = "Proceedings of the 3rd International Workshop on Satisfiability Checking and Symbolic Computation",

publisher = "CEUR Workshop Proceedings",

address = "Germany",

url = "http://www.sc-square.org/CSA/workshop3.html",

}

TY - GEN

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

AU - Mulligan, Casey

AU - Bradford, Russell

AU - Davenport, James H.

AU - England, Matthew

AU - Tonks, Zak

N1 - Conference code: 3

PY - 2018/9/1

Y1 - 2018/9/1

N2 - 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.

AB - 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.

M3 - Conference proceeding

BT - Proceedings of the 3rd International Workshop on Satisfiability Checking and Symbolic Computation

A2 - Bigatti, Anna M

A2 - Brain, Martin

PB - CEUR Workshop Proceedings

T2 - Third International Workshop on Satisfiability Checking and Symbolic Computation 2018

Y2 - 7 July 2018 through 9 July 2018

ER -

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

Abstract

Conference

Bibliographical note

Access to Document

Fingerprint

Cite this