Experimental Data on Relevance Filtering
Here you can download some of the data used for the experiments described in the paper "Lightweight Relevance Filtering for Machine-Generated Resolution Problems" by Paulson and Meng: specifically, the data for figures 15 to 17. The following items are available.
Thursday 12 January, 2012
- unfiltered and filtered versions of the 285 problems
- tab-delimited files comparing the success rates (unfiltered against filtered) as processor time rises from 10 to 300 seconds, for three provers:
Lawrence C. Paulson • Computer Laboratory • University of Cambridge