经济推理的量词消除
摘要：量词消除（QE）技术在经济学自动推理中的应用考虑。QE可以追溯到塔斯基在二十世纪四十年代的工作，而用于执行QE的软件则可以追溯到七十年代。已有大量的工作考虑了其在科学和工程中的应用，但我们在这里展示了它在社会科学中的应用。我们解释了经济学中许多推理定理可以通过自动化方式证明，甚至可以证明它们的假设是不一致的，并描述了这在经济学教育和研究中的应用。我们描述了从经济学文献中收集的一组QE示例，并指出这些示例的结构平均上与计算机代数文献中出现的结构有很大不同。这使我们建议基于常见的通用QE结果的结果记忆的新的渐进性QE方法。
作者：Casey B. Mulligan, Russell Bradford, James H. Davenport, Matthew England, and Zak Tonks
论文ID：1804.10037
分类：Symbolic Computation
分类简称：cs.SC
提交时间：2018-05-16