Arrow Research search

Author name cluster

Thomas Kolbe

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

4 papers
2 author rows

Possible papers

4

I&C Journal 2000 Journal Article

On Terminating Lemma Speculations

  • Christoph Walther
  • Thomas Kolbe

The improvement of theorem provers by reusing previously computed proofs is investigated. A method for reusing proofs is formulated as an instance of the problem reduction paradigm such that lemmata are speculated as proof obligations, being subject for subsequent reuse attempts. We motivate and develop a termination requirement, prove its soundness, and show that the reusability of proofs is not spoiled by the termination requirement imposed on the reuse procedure. Additional evidence for the general usefulness of the proposed termination order is given for lemma speculation in induction theorem proving.

Details DOI

AIJ Journal 2000 Journal Article

Proving theorems by reuse

  • Christoph Walther
  • Thomas Kolbe

We investigate the improvement of theorem proving by reusing previously computed proofs. We have developed and implemented the Plagiator system which proves theorems by mathematical induction with the aid of a human advisor: If a base or step formula is submitted to the system, it tries to reuse a proof of a previously verified formula. If successful, labour is saved, because the number of required user interactions is decreased. Otherwise the human advisor is called for providing a hand crafted proof for such a formula, which subsequently—after some (automated) preparation steps—is stored in the system's memory, to be in stock for future reasoning problems. Besides the potential savings of resources, the performance of the overall system is improved, because necessary lemmata might be speculated as the result of an attempt to reuse a proof. The success of the approach is based on our techniques for preparing given proofs as well as by our methods for retrieval and adaptation of reuse candidates which are promising for future proof reuses. We prove the soundness of our approach and illustrate its performance with several examples.

Details DOI
v2026.09.13