Datset Of Automated Economic Reasoning Problems For Qe / Smt

This dataset is generated by 45 economics theorems "A implies H" where A are assumptions and H a hypothesis. These are taken from textbooks and papers and chosen for their suitability for automatic solution with Quantifier Elimination (QE) or Satisfiability Modulo Theory (SMT) technology. For each theorem three problems are generated: checking the compatibility of the assumptions; checking for the existence of an example of the theorem; and checking for the existence of a counterexample. There are three files: 1. EconomicReasoningBenchmarks-Apr18-SMT2.zip This zip file will uncompress into a directory with 45 files, one for each theorem stating the three existence checks within the SMT2 format. Thus these files are suitable for use with any SMT solver supporting the theory. 2. EconomicReasoningBenchmarks-Apr20-Redlog.txt This plain text file can be run with the Redlog Package for the Computer Algebra System Reduce. It contains definitions and calls to Redlog's QE command to check for a counterexample for all 45 theorems. 3. EconomicReasoningBenchmarks-Apr23-Maple.txt This plain text file is for use with the Maple Computer Algebra System. For each theorem it provides the polynomials used in the Tarski formula to check for a counterexample. The polynomials are given as a list of lists with the outer list representing logical OR between entries and each inner list logical AND.本数据集基于45条经济学定理“A蕴含H”构建，其中A为假设集合，H为待验证假说。上述定理均取自教科书与学术论文，且均适配量词消去（Quantifier Elimination, QE）或可满足性模理论（Satisfiability Modulo Theory, SMT）技术的自动化求解任务。 针对每条定理，共生成三类检验问题：验证假设集合的相容性、验证该定理存在合法实例，以及验证是否存在反例。 本数据集包含三个文件： 1. EconomicReasoningBenchmarks-Apr18-SMT2.zip 该压缩包解压后将生成包含45个文件的目录，每个文件对应一条定理，以SMT2格式存储三类存在性检验内容，可兼容任意支持对应理论的SMT求解器。 2. EconomicReasoningBenchmarks-Apr20-Redlog.txt 该纯文本文件可通过计算机代数系统Reduce的Redlog包运行，其中包含了针对全部45条定理调用Redlog量词消去命令以验证反例的定义与调用语句。 3. EconomicReasoningBenchmarks-Apr23-Maple.txt 该纯文本文件适配Maple计算机代数系统。针对每条定理，其提供了塔斯基公式中用于验证反例的多项式：外层列表代表逻辑或关系，内层列表代表逻辑与关系，以嵌套列表形式给出。