This page contains supplementary material for the article “Monte Carlo Tableau Proof Search” submitted for CADE-26.

The current version of the paper is here.

Implementation

Here is the source code for the Monte Carlo Tree Search prover developed on top of leanCoP: Source

UPDATE 2017-03-04: Include Git history such that experiments can be actually run.

UPDATE 2017-03-30: Include Git tags to enable running of older experiments.

Note that the source code of other provers contained in the archive (FEMaLeCoP) has changed since previous publications.

Experimental results

The experiment descriptions are in eval/Makefile of the implementation. The output of the experiments is here: Output

Note that the uncompressed output of the experiment data is about 100GB. Therefore, it is recommended to selectively uncompress experiment data.