Hierarchical invention of targeted E prover strategies
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
SKEL
atp
examples
.gitignore
BliStrTune-RUN.sh
README.md
import-benchmark.sh
import-inits.sh
make-initprots.sh
setenv.sh

README.md

BliStrTune

Hierarchical invention of targeted E prover strategies

This is a pre-BETA release. It is usable with some effort.

Requirements

This distribution contains other software packages:

To run this software you need to have Python, Perl, and Ruby installed.

Quickstart

Prepare experiments

  1. Setup environment before running import scripts:

    $ . ./setenv.sh
    

    Always run the scripts from the BliStrTune directory.

  2. Import benchmark problems:

    $ ./import-benchmark.sh examples/bechmarks/test test  
    importing examples/bechmarks/test as test ... 10 problems imported
    
  3. Import initial protocols:

    $ ./import-inits.sh examples/inits/tptp tptp
    importing examples/inits/tptp as tptp ... 10 strategies imported
    

Setup experiments

$ vi BliStrTune-RUN.sh

Run experiments

$ ./BliStrTune-RUN.sh

Get results (optional)

$ BliStr-import-results.py BliStrTune-test-* test 1
$ expres-greedy.py test 1