Quantifier Elimination for Reasoning in Economics

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

Research output: Other contribution


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.
Original languageEnglish
Publication statusPublished - 26 Apr 2018


  • Quantifer Elimination
  • Symbolic Computation


Dive into the research topics of 'Quantifier Elimination for Reasoning in Economics'. Together they form a unique fingerprint.

Cite this