The motivation behind this thesis is to formally prove programs correct. The contributions are twofold:Firstly, a new rule of mathematical induction called collage induction, is introduced, which treats mathematical induction as a natural generalization of the CUT-rule. Conceptually the rule can be understood as follows: To prove an implication G ? D, an inductively defined property p is constructed such that G ? p. The implication p ? D is then proved by induction according to the definition of p.Secondly, a program synthesis method for extracting programs from proofs in Extended Execution, is generalized to allow the relations defining p to be synthesized from the proof of an induction lemma.