The search result changed since you submitted your search request. Documents might be displayed in a different sort order.
  • search hit 2 of 2
Back to Result List

Reusing Proofs

  • We develop a learning component for a theorem prover designed for verifying statements by mathematical induction. If the prover has found a proof, it is analyzed yielding a so-called catch. The catch provides the features of the proof which are relevant for reusing it in subsequent verification tasks and may also suggest useful lemmata. Proof analysis techniques for computing the catch are presented. A catch is generalized in a certain sense for increasing the reusability of proofs. We discuss problems arising when learning from proofs and illustrate our method by several examples.

Download full text files

Export metadata

Additional Services

Share in Twitter Search Google Scholar
Author:Thomas Kolbe, Christoph Walther
URN (permanent link):urn:nbn:de:hbz:386-kluedo-1499
Document Type:Preprint
Language of publication:English
Year of Completion:1999
Year of Publication:1999
Publishing Institute:Technische Universität Kaiserslautern
Date of the Publication (Server):2000/04/03
Tag:learning; theorem prover
This work was supported under grants no. Wa652/4-1,2 by the Deutsche Forschungsgemeinschaft as part of the focus program "Deduktion".2
Faculties / Organisational entities:Fachbereich Informatik
DDC-Cassification:0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik
Licence (German):Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011