Stephan Schulz, Andreas Kuechler, Christoph Goller: "Some Experiments
on the Applicability of Folding Architecture Networks to Guide Theorem
Proving"

Abstract:

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.