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.