# TheoryGuru: A Mathematica Package to apply Quantifier Elimination

arXiv: https://arxiv.org/abs/1806.10925 · HTML: https://mlsanity.com/paper/1806.10925/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 28 Jun 2018.

## Built on by (most cited first, 3 of 3)

- [Explainable AI Insights for Symbolic Computation: A case study on selecting the variable ordering for cylindrical algebraic decomposition](https://mlsanity.com/paper/2304.12154/) (2023)
- [Data Augmentation for Mathematical Objects](https://mlsanity.com/paper/2307.06984/) (2023)
- [Constrained Neural Networks for Interpretable Heuristic Creation to Optimise Computer Algebra Systems](https://mlsanity.com/paper/2404.17508/) (2024)

## Abstract (arXiv)

We consider the use of Quantifier Elimination (QE) technology for automated reasoning in economics. There is a great body of work considering QE applications in science and engineering but we demonstrate here that it also has use 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 via QE. However, economists who this technology could benefit are usually unfamiliar with QE, and the use of mathematical software generally. This motivated the development of a Mathematica Package TheoryGuru, whose purpose is to lower the costs of applying QE to economics. We describe the package's functionality and give examples of its use.