A constructive proving system and the method of combining deduction with knowledge are presented for program synthesis. The synthesis of nondeterministic logic programs is discussed. An example of synthesis of Prolog program "append" is given to illustrate our method.