A Feature-Based Learning Method for Theorem Proving

Matthias Fuchs

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 areal 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.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.