@InProceedings{C9,
  key    =       {C09},
  author =	 {Mateja Jamnik and Manfred Kerber and Christoph Benzm{\"u}ller},
  title =	 {Towards Learning New Methods in Proof Planning},
  booktitle =	 {Symbolic Computation and Automated Reasoning},
  year =	 2000,
  pages =        {142-159},
  editor =       {Manfred Kerber and Michael Kohlhase},
  chrisnote =	 {C9},
  publisher =	 {A.K.Peters},
  url =		 {www.ags.uni-sb.de/~chris/papers/C9.pdf},
  abstract =	 {In this paper we propose how proof planning systems can be extended by
                  an automated learning capability. The idea is that a proof planner would
                  be capable of learning new proof methods from well chosen examples of
                  proofs which use a similar reasoning strategy to prove related theorems,
                  and this strategy could be characterised as a proof method. We propose a
                  representation framework for methods, and a machine learning technique
                  which can learn methods using this representation framework. The
                  technique can be applied (amongst other) to learn whether and when to
                  call external systems such as theorem provers or computer algebra
                  systems. This is work in progress, and we hope to gain useful feedback
                  from the CALCULEMUS community.}
}


