Quantifier Elimination over Finite Fields Using Gr\"obner Bases

Andr\'e Platzer; Edmund M. Clarke; Sicun Gao

REVIEW

Quantifier Elimination over Finite Fields Using Gr\"obner Bases

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1104.0746 v1 pith:5NBVKN2V submitted 2011-04-05 cs.SC cs.LO

Sicun Gao , André Platzer , Edmund M. Clarke This is my paper

classification cs.SCcs.LO

keywords algorithmeliminationfinitefieldsobnerquantifieralgebraicanalysis

verification ladder T0 review T1 audit T2 compute T3 formal

0 comments

read the original 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.

Discussion (0). Sign in to comment.

Pith tools