Quantifier Elimination over Finite Fields Using Gröbner Bases

Sicun Gao, André Platzer, Edmund M. Clarke

We give an algebraic quantifier elimination algorithm for the first-order theory over any given finite field using Gröbner basis methods. The algorithm relies on the strong Nullste…