Quantifier Elimination over Finite Fields Using Gr\"obner Bases

TL;DR

This paper presents an algebraic quantifier elimination algorithm for finite fields utilizing Gr"obner bases, enabling formal analysis of models such as biological controllers.

Contribution

It introduces a novel algorithm based on Gr"obner bases and Nullstellensatz for quantifier elimination over finite fields, with complexity analysis and practical application.

Findings

Algorithm successfully performs quantifier elimination over finite fields.

Complexity analysis provides insights into the algorithm's efficiency.

Application demonstrates utility in biological controller model analysis.

Abstract

We give an algebraic quantifier elimination algorithm for the first-order theory over any given finite field using Gr\"obner 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.