A feature-based learning method for theorem proving
Matthias Fuchs · National Conference on Artificial Intelligence · 1998
Automated reasoning or theorem proving essentially amounts to solving search problems. Despite significant progress in recent years theorem provers still have many shortcomings. The use of machine-learning techniques is acknowledged as promising, but difficult to apply in the area of theorem proving. We propose here to learn search-guiding heuristics by employing features in a simple, yet effective manner. Features are used to adapt a heuristic to a solved source problem. The adapted heuristic can then be utilized profitably for solving related target problems. Experiments have demonstrated that the approach not only allows for significant speed-ups, but also makes it possible to prove problems that were out of reach before.