Experiments in the Heuristic Use of Past Proof Experience

Abstract

Problems stemming from the study of logic calculi in connection with an inference rule called “condensed detachment” are widely acknowledge as prominent test sets for automated deduction systems and their search guiding heuristics. It is in the light of these problems that we demonstrate the power of heuristics that make use of past proof experience with numerous experiments. We present two such heuristics. The first heuristic attempts to re-enact a proof of a proof problem found in the past in a flexible way in order to find a proof of a similar problem. The second heuristic employs “features” in connection with past proof experience to prune the search space. Both these heuristics not only allow for substantial speed-ups, but also make it possible to prove problems that were out of reach when using so-called basic heuristics. Moreover, a combination of these two heuristics can further increase performance. We compare our results with the results the creators of OTTER obtained with this renowned theorem prover and this way substantiate or achievements.