We present a method for proving properties of de®nite logic programs. This method is called unfold/fold proof method because it is based on the unfold/fold transformation rules. Given a program and two goals (that is, conjunctions of atoms) p Y and q Y , where , , and are pairwise disjoint vectors of variables, the unfold/fold proof method can be used to show that the equivalence formula V W p Y 6 W q Y holds in the least Herbrand model of . Equivalence formulas of that form can be used to justify goal replacement steps, which allow us to transform logic programs by replacing old goals, such as p Y , by equivalent new goals, such as q Y . These goal replacements preserve the least Herbrand model semantics if we ®nd non-ascending unfold/fold proofs of the corresponding equivalence formulas, that is, unfold/fold proofs which ensure suitable well-founded orderings between the successful SLD-derivations of p Y and q Y , respectively. We also present a method for program synthesis from implicit de®nitions. It can be used to derive a de®nite logic program for the predicate newp implicitly de®ned by an equivalence formula of the form V W p Y 6 W r Y Y newp Y , such that the predicates occurring in the goals p Y and r Y are de®ned in a given program , and newp is a predicate symbol not occurring in . The set of clauses de®ning newp, say Eureka, allows us to prove that the above equivalence formula holds in the least Herbrand model of iurek using an unfold/fold proof. Thus, the correctness of our synthesis method derives from the one of the unfold/fold proof method. We ®nally illustrate our synthesis method through some examples of program specialization, program synthesis, and program transformation, which can all be viewed as program syntheses from implicit de®nitions.