An iterative and bottom-up procedure for proving-by-example

Abstract

We give a procedure for generalizing a proof of a concrete instance of a theorem by recovering inductions that have been expanded in the concrete proof. It consists of three operations introduction, extension and propagation, and by iterating these operations in a bottom-up fashion, it can reconstruct nested inductions. We discuss how to use EBG for identifying the induction formula, and how EBG must be modified so that nested inductions can be reconstructed.