Quantifier Elimination over Finite Fields Using Gröbner Bases

Abstract

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 Nullstellensatz and properties of elimination ideals over finite fields. We analyze the theoretical complexity of the algorithm and show its application in the formal analysis of a biological controller model.

A shorter version is to appear in International Conference on Algebraic Informatics 2011

References in corpus (1)

• Reverse-engineering of polynomial dynamical systems

Cited by in corpus (4)

• Linear and non-linear relational analyses for Quantum Program Optimization
• An Algebraic Model For Quorum Systems
• Classifier construction in Boolean networks using algebraic methods
• The Number of Gröbner Bases in Finite Fields