Quantifier Elimination for Reasoning in Economics

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

Research output: Other contribution

Abstract

We consider the use of Quantifier Elimination (QE) technology for automated reasoning in economics. QE dates back to Tarski's work in the 1940s with software to perform it dating to the 1970s. There is a great body of work considering its application in science and engineering but we show here how it can also find application 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; and describe the application of this in both economics education and research. We describe a bank of QE examples gathered from economics literature and note the structure of these are, on average, quite different to those occurring in the computer algebra literature. This leads us to suggest a new incremental QE approach based on result memorization of commonly occurring generic QE results.
LanguageEnglish
StatusPublished - 26 Apr 2018

Keywords

  • Quantifer Elimination
  • Symbolic Computation

Cite this

Quantifier Elimination for Reasoning in Economics. / Mulligan, Casey B.; Bradford, Russell; Davenport, James; England, Matthew; Tonks, Zak.

2018, .

Research output: Other contribution

@misc{81715a933d484037b0b63f0ace480985,
title = "Quantifier Elimination for Reasoning in Economics",
abstract = "We consider the use of Quantifier Elimination (QE) technology for automated reasoning in economics. QE dates back to Tarski's work in the 1940s with software to perform it dating to the 1970s. There is a great body of work considering its application in science and engineering but we show here how it can also find application 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; and describe the application of this in both economics education and research. We describe a bank of QE examples gathered from economics literature and note the structure of these are, on average, quite different to those occurring in the computer algebra literature. This leads us to suggest a new incremental QE approach based on result memorization of commonly occurring generic QE results.",
keywords = "Quantifer Elimination, Symbolic Computation",
author = "Mulligan, {Casey B.} and Russell Bradford and James Davenport and Matthew England and Zak Tonks",
year = "2018",
month = "4",
day = "26",
language = "English",
type = "Other",

}

TY - GEN

T1 - Quantifier Elimination for Reasoning in Economics

AU - Mulligan, Casey B.

AU - Bradford, Russell

AU - Davenport, James

AU - England, Matthew

AU - Tonks, Zak

PY - 2018/4/26

Y1 - 2018/4/26

N2 - We consider the use of Quantifier Elimination (QE) technology for automated reasoning in economics. QE dates back to Tarski's work in the 1940s with software to perform it dating to the 1970s. There is a great body of work considering its application in science and engineering but we show here how it can also find application 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; and describe the application of this in both economics education and research. We describe a bank of QE examples gathered from economics literature and note the structure of these are, on average, quite different to those occurring in the computer algebra literature. This leads us to suggest a new incremental QE approach based on result memorization of commonly occurring generic QE results.

AB - We consider the use of Quantifier Elimination (QE) technology for automated reasoning in economics. QE dates back to Tarski's work in the 1940s with software to perform it dating to the 1970s. There is a great body of work considering its application in science and engineering but we show here how it can also find application 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; and describe the application of this in both economics education and research. We describe a bank of QE examples gathered from economics literature and note the structure of these are, on average, quite different to those occurring in the computer algebra literature. This leads us to suggest a new incremental QE approach based on result memorization of commonly occurring generic QE results.

KW - Quantifer Elimination

KW - Symbolic Computation

M3 - Other contribution

ER -