Exploiting past proof experience
Matthias Fuchs · 1999
We are going to present two methods that allow to exploit previous experience in the area of automated deduction. The first method adapts (learns) the parameters of a heuristic employed for controlling the application of inference rules in order to find a known proof with as little redundant search effort as possible. Adaptation is accomplished by a genetic algorithm. A heuristic learned that way can then be profitably used to solve similar problems. The second method attempts to re-enact a known proof in a flexible manner in order to solve an unknown problem whose proof is believed to lie in (close) vicinity. The experimental results obtained with an equational theorem prover show that these methods not only allow for impressive speed-ups, but also make it possible to handle problems that were out of reach before.