Supporting Documents for Real Algebraic Strategies for MetiTarski Proofs

• To compile MetiTarski, you need the Poly/ML Standard ML compiler version 5.4.1 or later.

• MetiTarski source code: metis-rcf.zip.
  To build: Type make within the metis-rcf/ subdirectory.

• Within the MetiTarski archive, the collection of all (~840) benchmark problems is under the metis-rcf/tptp/Problems/ subdirectory.
  The axioms MetiTarski uses to reason about non-polynomial functions may be found under the metis-rcf/tptp/Axioms/ subdirectory.

• As described in our paper, the experiments were done w.r.t. a subset of our benchmark problems, those which MetiTarski, before the work in our paper, could not solve in under one second.
  This subset of 409 problems is here: cicm-tptp.zip.

• In the paper, the names of the problems listed in our figures match the filenames in this problem archive.
  For instance, the MetiTarski input problem corresponding to the problem listed in the paper as tan-1-1var-weak is the file tan-1-1var-weak.tptp.

• As described in our paper, in searching for a proof of an input problem P (involving transcendental functions), MetiTarski generates a sequence of RCF subproblems.
  The collection of RCF subproblems MetiTarski generates in its search for each benchmark problem considered is here: rcf-traces.zip.
  For instance, the sequence of RCF subproblems generated during MetiTarski's search for a proof for tan-1-1var-weak.tptp (contained in cicm-tptp.zip) is given in the file tan-1-1var-weak.trace (contained in rcf-traces.zip).
  For each RCF subproblem listed in each trace file, we give translations of the RCF subproblem into Mathematica, QEPCAD-B and Z3 (SMTLib 2.0) syntax.
  For example: A MetiTarski problem - tan-1-1var-weak.tptp - and its trace file of RCF subproblems - tan-1-1var-weak.trace.

• A Mac OS X Z3 binary used in the experiments in our paper is here: Z3_nonlin_cambridge_mac.zip.
  (Binaries for other architectures can be built if requested.)

• To run MetiTarski upon a problem foo.tptp:
  • With QEPCAD-B as RCF engine:

    metit foo.tptp

  • With Mathematica 8.* as RCF engine:

    metit -m foo.tptp

  • With plain Z3_nonlin (univariate factorisation enabled, no model-sharing) as RCF engine:

    metit --smt foo.tptp

  • With `Strategy 1' (Z3_nonlin, univariate factorisation disabled, with model-sharing) as RCF engine:

    metit --strategy 1 foo.tptp

• By default, MetiTarski will output a log of its proof search, and terminate with its judgment as to the truth of the input problem.
  To get MetiTarski to output a proof for a theorem, use the -p option.
  MetiTarski outputs proofs in a variant of the TSTP standard format (cf. http://www.cs.miami.edu/~tptp/TSTP/ for more).
  For instance:

  metit -p --strategy 1 tan-1-1var-weak.tptp > tan-1-1var-weak.proof

  yields the following MetiTarski proof of the problem tan-1-1var-weak.tptp: tan-1-1var-weak.proof.

• Running metit with no options will give a description of supported command line arguments.
  Note that certain environment variables must be setup to run MetiTarski: a $TPTP environment variable pointing to the metis-rcf/tptp/ subdirectory, and special environment variables for interfacing with QEPCAD-B, Mathematica and Z3.
  Until these are setup, MetiTarski will generate error messages to guide the user through setting these environment variables correctly.

• There is a script, metis-rcf/scripts/runmetit which allows one to run MetiTarski against a benchmark set and record experimental results.
  For instance, to run MetiTarski, using Strategy 1, against all problems considered in the paper, with a time limit of 120 seconds:
  1. Change to the subdirectory containing all problems in cicm-tptp.zip.

  2. Let $MT_SCRIPTS be the metis-rcf/scripts subdirectory.

  3. Execute: $MT_SCRIPTS/runmetit --time=120 --options='--strategy 1'

  This process produces a log file with a name of the form STATUS-Metit-‹DATE›-‹TIME_LIMIT›--‹OPTIONS›.log.
  For instance, if run on 28-Feb-2012, the above command would generate a log file named STATUS-Metit-2012-02-28-120--strategy_1.log.

  The script metis-rcf/scripts/compare-logfiles.pl can be used to compare multiple log files, reporting, for each considered theorem, which log file contains the fastest proof of the theorem by at least some specified margin. This is how the bar graphs in Fig. 2 were created.

• Please let us know if any more information would be helpful.