Experiments in the Heuristic Use of Past Proof Experience

Matthias Fuchs
Fachbereich Informatik, Universitaet Kaiserslautern
Postfach 3049, 67653 Kaiserslautern
Germany
E-mail: fuchs@informatik.uni-kl.de

Abstract
Problems stemming from the study of logic calculi
in connection with an inference
rule called ``condensed detachment'' are widely acknowledged 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 our achievements.

Keywords
automated deduction, condensed detachment, learning

Source
anonymous FTP server ftp.uni-kl.de [131.246.94.94]
path: /reports_uni-kl/computer_science/SEKI/1995/
file: Fuchs.SR-95-10.ps.gz