@inproceedings{C9,
  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.},
  Author =	 {Mateja Jamnik and Manfred Kerber and Christoph
                  Benzm{\"u}ller},
  Booktitle =	 {Symbolic Computation and Automated Reasoning},
  Editor =	 {Manfred Kerber and Michael Kohlhase},
  Keywords =	 {own, CALCULEMUS, Symb. Computation and
                  Symb. Reasoning, Proof Planning, Machine Learning},
  Pages =	 {142-159},
  Publisher =	 {A.K.Peters},
  Title =	 {Towards Learning New Methods in Proof Planning},
  url_preprint = {http://christoph-benzmueller.de/papers/C9.pdf},
  Year =	 2000,
}

{"_id":"59Mfy2s8fCLF29YSm","bibbaseid":"jamnik-kerber-benzmller-towardslearningnewmethodsinproofplanning-2000","author_short":["Jamnik, M.","Kerber, M.","Benzmüller, C."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","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.","author":[{"firstnames":["Mateja"],"propositions":[],"lastnames":["Jamnik"],"suffixes":[]},{"firstnames":["Manfred"],"propositions":[],"lastnames":["Kerber"],"suffixes":[]},{"firstnames":["Christoph"],"propositions":[],"lastnames":["Benzmüller"],"suffixes":[]}],"booktitle":"Symbolic Computation and Automated Reasoning","editor":[{"firstnames":["Manfred"],"propositions":[],"lastnames":["Kerber"],"suffixes":[]},{"firstnames":["Michael"],"propositions":[],"lastnames":["Kohlhase"],"suffixes":[]}],"keywords":"own, CALCULEMUS, Symb. Computation and Symb. Reasoning, Proof Planning, Machine Learning","pages":"142-159","publisher":"A.K.Peters","title":"Towards Learning New Methods in Proof Planning","url_preprint":"http://christoph-benzmueller.de/papers/C9.pdf","year":"2000","bibtex":"@inproceedings{C9,\n Abstract =\t {In this paper we propose how proof planning systems\n can be extended by an automated learning\n capability. The idea is that a proof planner would\n be capable of learning new proof methods from well\n chosen examples of proofs which use a similar\n reasoning strategy to prove related theorems, and\n this strategy could be characterised as a proof\n method. We propose a representation framework for\n methods, and a machine learning technique which can\n learn methods using this representation\n framework. The technique can be applied (amongst\n other) to learn whether and when to call external\n systems such as theorem provers or computer algebra\n systems. This is work in progress, and we hope to\n gain useful feedback from the CALCULEMUS community.},\n Author =\t {Mateja Jamnik and Manfred Kerber and Christoph\n Benzm{\\\"u}ller},\n Booktitle =\t {Symbolic Computation and Automated Reasoning},\n Editor =\t {Manfred Kerber and Michael Kohlhase},\n Keywords =\t {own, CALCULEMUS, Symb. Computation and\n Symb. Reasoning, Proof Planning, Machine Learning},\n Pages =\t {142-159},\n Publisher =\t {A.K.Peters},\n Title =\t {Towards Learning New Methods in Proof Planning},\n url_preprint = {http://christoph-benzmueller.de/papers/C9.pdf},\n Year =\t 2000,\n}\n\n","author_short":["Jamnik, M.","Kerber, M.","Benzmüller, C."],"editor_short":["Kerber, M.","Kohlhase, M."],"key":"C9","id":"C9","bibbaseid":"jamnik-kerber-benzmller-towardslearningnewmethodsinproofplanning-2000","role":"author","urls":{" preprint":"http://christoph-benzmueller.de/papers/C9.pdf"},"keyword":["own","CALCULEMUS","Symb. Computation and Symb. Reasoning","Proof Planning","Machine Learning"],"metadata":{"authorlinks":{}},"html":""},"bibtype":"inproceedings","biburl":"http://page.mi.fu-berlin.de/cbenzmueller/papers/chris.bib","dataSources":["ckRabafyoGpACyPpf","S5G7BggtbXZA2Q63T"],"keywords":["own","calculemus","symb. computation and symb. reasoning","proof planning","machine learning"],"search_terms":["towards","learning","new","methods","proof","planning","jamnik","kerber","benzmüller"],"title":"Towards Learning New Methods in Proof Planning","year":2000}