Automatic Acquisition of Search Control Knowledge from
                        Multiple Proof Attempts

                   Joerg Denzinger
                   Stephan Schulz

  We present two inference control heuristics for equational deduction
  that are based on the evaluation of previous successful proof attempts
  in domains of interest. The first evaluation function works by symbolic
  retrieval of generalized patterns from a knowledge base, the second
  function compiles the knowledge into abstract term evaluation trees.
  Both heuristics have been implemented into the distributed equational proof
  system DISCOUNT. We analyze the performance of the heuristics on
  several sets of examples (including the subset of all unit-equality
  problems from the TPTP collection) and demonstrate their usefulness.