§ Formal Verification of Multiplier Circuits using Computer Algebra

We show how the polynomial calculus can be instantiated to yield a
practical algebraic calculus (PAC).

For this optimization we introduce the necessary theory and present
a technical theorem that allows us to rewrite only local parts of the Gröbner
basis in such a way that the result is again a Gröbner basis.

Because of Buchberger’s product criterion
and the structure of the gate polynomials, the gate polynomials together with the Boolean
value constraints define a Gröbner basis for the ideal generated by the gate polynomials
and Boolean value constraints.