A lot of the human ability to prove hard mathematical theorems can be ascribed to a domain-specific problem solving know-how. Such knowledge is intrinsically incomplete. In order to solve related problems, human mathematicians can go beyond their acquired knowledge by adapting their know-how. These two aspects, having rich experience and extending it by need, can be simulated in a proof planning framework. The domain-specific reasoning knowledge is represented in form of declarative planning operators, called methods. Since these are declarative, they can be mechanically adapted to new situations by so-called meta-methods. In this contribution we apply this framework to two prominent proofs in theorem proving. First, we present methods for proving the ground completeness of binary resolution, which essentially correspond to key lemmata, and then, we show how these methods can be reused for the proof of the ground completeness of lock resolution.
Proof planning, reuse, adaptation