Authors  : Joerg Denzinger, Matthias Fuchs, Christoph Goller,
           Stephan Schulz
Titel    : Learning from Previous Proof Experience: A Survey
Report#  : AR-99-4
Date     : 10.12.1999
Keywords : learning, theorem proving, heuristic, search control,
           analogy  

                         Abstract 

  We present an overview of various learning techniques used in
  automated theorem provers. We characterize the main problems arising
  in this context and classify the solutions to these problems from
  published approaches.
  We analyze the suitability of several combinations of solutions for
  different approaches to theorem proving and place these combinations
  in a spectrum ranging from provers using very specialized learning
  approaches to optimally adapt to a small class of proof problems, to
  provers that learn more general kinds of knowledge, resulting in 
  systems that are less efficient in special cases but show improved
  performance for a wide range of problems.  Finally, we suggest
  combinations of solutions for various proof philosophies.