Stephan Schulz and Felix Brandt: "Using Term Space Maps to Capture
Search Control Knowledge in Equational Theorem Proving"

Abstract:

We describe a learning inference control heuristic for an equational
theorem prover. The heuristic selects a number of problems similar to
a new problem from a knowledge base and compiles information about
good search decisions for these selected problems into a \emph{term
space map}, which is used to evaluate the search alternatives at an
important choice point in the theorem prover.  Experiments on the TPTP
problem library show the improvements possible with this new approach.