Choosing an appropriate search-guiding heuristic in order to solve a problem with an automated deduction system is in general a difficult task. We propose to automate this choice using a machine-learning approach closely related to instance-based learning and nearest-neighbor classification. In experimental studies the approach has produced very promising results.
instance-based learning, nearest-neighbor rule, automated deduction