Datset of automated economic reasoning problems for QE / SMT (Q6698790)

This dataset is generated by45 economics theorems A implies H where A are assumptions and H a hypothesis. These are takenfrom textbooks and papers and chosen for their suitabilityfor automatic solution with Quantifier Elimination (QE) or Satisfiability Modulo Theory (SMT) technology. For each theorem three problems are generated: checking the compatibilityof the assumptions; checking for the existenceof anexample of the theorem; and checking for the existence of a counterexample. There are threefiles: 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 Redlogs 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 theoremit provides the polynomials used in the Tarski formula to check for a counterexample. The polynomials are given as a listof lists with the outer list representing logical OR between entries and each inner list logical AND.