Quantifier elimination over finite fields using Gröbner bases

DOI10.1007/978-3-642-21493-6_9MaRDI QIDQ3014937zbMATH OpenOpenAlexFDO

Authors Sicun Gao, André Platzer, Edmund Clarke

Publication date 8 July 2011

Published in Algebraic Informatics (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1104.0746

Mathematics Subject Classification ID

Quantifier elimination, model completeness, and related topics (03C10) Finite fields (field-theoretic aspects) (12E20) Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) (13P10) Symbolic computation and algebraic computation (68W30)

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.

Recommendations

• A formal quantifier elimination for algebraically closed fields
• scientific article; zbMATH DE number 4014674
• scientific article; zbMATH DE number 871442
• On the combinatorial and algebraic complexity of quantifier elimination
• scientific article; zbMATH DE number 3918343

Cites work

• scientific article; zbMATH DE number 1273642 (Why is no real title available?)
• scientific article; zbMATH DE number 493127 (Why is no real title available?)
• scientific article; zbMATH DE number 2165490 (Why is no real title available?)
• Model Theory
• Reverse-engineering of polynomial dynamical systems

Cited in

(6)

• Quantifier elimination for Henselian fields relative to additive and multiplicative congruences
• Elimination of constants from machines over algebraically closed fields
• QE software based on comprehensive Gröbner systems
• The number of Gröbner bases in finite fields (research)
• SMT solving over finite field arithmetic
• Quantifier elimination in linear difference equations over Witt vectors

This page was built for publication: Quantifier elimination over finite fields using Gröbner bases

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3014937)