Quantifier Elimination over Finite Fields Using Gr\"obner Bases
Symbolic Computation
2018-05-01 v1 Logic in Computer Science
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.
Keywords
Cite
@article{arxiv.1104.0746,
title = {Quantifier Elimination over Finite Fields Using Gr\"obner Bases},
author = {Sicun Gao and André Platzer and Edmund M. Clarke},
journal= {arXiv preprint arXiv:1104.0746},
year = {2018}
}
Comments
A shorter version is to appear in International Conference on Algebraic Informatics 2011