从经济学的自动推理中得出的非线性实数算术基准
摘要：自动化解决经济学问题的数学软件中，我们考虑到的问题。我们提出并免费提供了一个新的基准问题集。已经证明这些问题属于非线性实数算术框架，并且在计算机代数系统中通常通过量词消除（QE）技术可以解决。此外，它们都可以用前束范式表达，仅包含存在量词，并且支持QF_NRA的可满足性模块理论（SMT）求解器也可以处理。已经有大量的工作在考虑使用QE和SMT在科学和工程上的应用，但我们在这里展示了这项技术在社会科学中也有潜力。
作者：C. Mulligan, R. Bradford, J.H. Davenport, M.England and Z. Tonks
论文ID：1806.11447
分类：Symbolic Computation
分类简称：cs.SC
提交时间：2018-11-01