Automated Economic Reasoning with Quantifier Elimination

Casey Mulligan

No 22922, NBER Working Papers from National Bureau of Economic Research, Inc

Abstract: Many theorems in economics can be proven (and hypotheses shown to be false) with “quantifier elimination.” Results from real algebraic geometry such as Tarski’s quantifier elimination theorem and Collins’ cylindrical algebraic decomposition algorithm are applicable because the economic hypotheses, especially those that leave functional forms unspecified, can be represented as systems of multivariate polynomial (sic) equalities and inequalities. The symbolic proof or refutation of economic hypotheses can therefore be achieved with an automated technique that involves no approximation and requires no problem-specific information beyond the statement of the hypothesis itself. This paper also discusses the computational complexity of this kind of automated economic reasoning, its implementation with Mathematica and REDLOG software, and offers several examples familiar from economic theory.

JEL-codes: B41 C63 C65 (search for similar items in EconPapers)
Date: 2016-12
New Economics Papers: this item is included in nep-cmp
Note: IO PE TWP
References: View references in EconPapers View complete reference list from CitEc
Citations: View citations in EconPapers (1)

Downloads: (external link)
http://www.nber.org/papers/w22922.pdf (application/pdf)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:nbr:nberwo:22922

Ordering information: This working paper can be ordered from
http://www.nber.org/papers/w22922

Access Statistics for this paper

More papers in NBER Working Papers from National Bureau of Economic Research, Inc National Bureau of Economic Research, 1050 Massachusetts Avenue Cambridge, MA 02138, U.S.A.. Contact information at EDIRC.
Bibliographic data for series maintained by ().