In this talk we present a constraint logic framework that combines backward and forward chaining. Concretely in this framework coexist two kinds of rules: On the one some rules —which corresponds to CLP clauses— are processed by backward chaining, while on the other hand the others rules —which generalize constraint propagation rules– are processed by forward chaining. We then illustrate how commutation of the backward rules with respect to the forward rules can be used to automate inductive proofs over CLP programs.