Automatic acquisition of search control knowledge from multiple proof attempts

We present two inference control heuristics for equational deduction that a re 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, and the second function compile s the knowledge into abstract term evaluation trees. Both heuristics have b een implemented into the distributed equational proof system DISCOUNT. We a nalyze the performance of the heuristics on several sets of examples (inclu ding the subset of all unit-equality problems from the TPTP collection) and demonstrate their usefulness. (C) 2000 Academic Press.