One of the major problems in theorem proving is control of the proof search. A promising approach is the application of machine learning techniques for the acquisition of search control knowledge by learning from successful proof searches. In this paper we briefly discuss this idea and existing machine learning techniques for this task. We suggest neural folding architecture networks together with supervised training algorithms as a very promising candidate for learning search control knowledge. This suggestion is based on two sets of experiments in which we applied folding architecture networks to term ordering problems and clause classification tasks resulting from the proof search of the equational theorem prover DISCOUNT.
Neural Networks, Connectionist Structure Processing, Heuristics
for Theorem Provers, Term orderings