A Feature-Based Learning Method for Theorem Proving

Automatedreasoning or theorem proving essentially amounts to solving search problems. Despite significant progress in recent years theorem provers still have manyshortcomings. The use of machine-learning techniques is acknowledgedas promising, but difficult to apply in the area of theorem proving. Wepropose 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 makesit possible to prove problems that were out of reach before.

• Type: Conference
• Year: 1998
• Where: AAAI
• Authors: Matthias Fuchs
• Keywords: AAAI 1998, Intelligent Agents, Search Problems, Significant Progress, Theorem Proving