Making programs redundancy-free, an important problem of automatic program generation, is dealt with by proving the logical formula describing their I/O behavior with natural deduction. The discussion applies a simple, artificial programming language to simplify the complicated technique. The constructive logic used here is an intuitionistic version of first-order natural deduction with mathematical induction.

The author intends to minimize the information needed from the user (who gives the formula describing the function to be implemented--the so-called end-formula of the proof-tree). Having proven the end-formula, the user gets the generated sequence of the realizing variables, which are introduced to keep track of realizing codes for the formula. (For each existential or disjunctive subformula of the end-formula, a realizing variable is generated.) The user has to select those components of the realizing sequence that are interesting in case of a special application of the end-formula.

The paper describes a basic and an improved variant of the proof tree marking and code extraction procedure. It thoroughly discusses the problems raised by the application of induction (sometimes it is necessary to generalize both the formulae and the corresponding realizing sequences in order to be able to prove them by induction), and proposes a solution for generalizing realizing variable sequences.

Notwithstanding that the notions and methods are illustrated by examples, the technical complexity, the occasional lack of explanation, and a few misprints make the paper rather hard to follow.