Dataset 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.