We give here an effective proof of Hilbert's nullstellensatz and Krivine-Stengle's positivestellensatz using the cut elimination theorem for sequent calculus. The proof is very similar to the current techniques in constructive algebraic geometry by Henri Lombardi, but seems more modular.

In the case of the positive stellensatz, we think we prove a more general result than the original one, thanks to a new notion of justification of positiveness: PBDD (polynomial binary decision diagram). It allows both to recover Krivine-Stengle's justification, but also another one which seems to require lower degree.

We apply the same techniques to the nullstellensatz for differentially closed field and show that the proof is almost unchanged.

Remark: here we do not provide bound, but an effective algorithm (implemented in OCaml) to build the wanted algebraic equality. Nevertheless, we discuss how bound could probably be obtained. We also do not deal effectively with the axiom of algebraic/real closure. Those are eliminated using standard model theory.