Patching Proofs for Reuse

. 1 We investigate the application of machine learning paradigms in automated reasoning in order to improve a theorem prover by reusing previously computed proofs. Our reuse procedure generalizes a previously computed proof of a conjecture yielding a schematic proof which can be instantiated subsequently if a new, similar conjecture is given. We show that for exploiting the full flexibility of second-order instantiations the instantiated schematic proof has to be patched such that a proof of the new conjecture is obtained. We develop an algorithm which computes patched proofs showing thereby that proof patching is always possible in a uniform way. This enables a further processing of the obtained proof, justifies the soundness of our proposal for reusing proofs, and provides a key for comparing our method with other reuse paradigms. 1 Introduction Several machine learning paradigms aim to improve a problem solver by reusing previously computed solutions, e.g. explanation-based learn..