Title
An efficient quantifier elimination algorithm for algebraically closed fields of any characteristic
Abstract
An Algorithm is given which, as input, accepts a formula ϕ in prenex normal form, with prime formulas P=o, P≠o, for P ε Z [x1,...,x1], and some r ε N. It produces a quantifierfree formula ψ in disjunctive normal form (DNF) such that, in any algebraically closed field, ϕ ψ is true. The time required for a formula of length l with q quantifiers and r-q free variables is bounded by (c1·l) cr2 rq, for some constants c1, c2. If no ∀-quantifiers occur and the matrix of ϕ is in DNF, then the time is bounded by (c1·l)rcq2.
Year
DOI
Venue
1975
10.1145/1088322.1088324
ACM SIGSAM Bulletin
Keywords
Field
DocType
q quantifiers,prime formula,quantifierfree formula,cr2 rq,r-q free variable,disjunctive normal form,prenex normal form,length l,efficient quantifier elimination algorithm,constants c1,normal form,quantifier elimination
Prime (order theory),Quantifier elimination,Discrete mathematics,Combinatorics,Matrix (mathematics),Free variables and bound variables,Prenex normal form,Disjunctive normal form,Algorithm,Mathematics,Algebraically closed field,Bounded function
Journal
Volume
Issue
Citations 
9
4
3
PageRank 
References 
Authors
7.48
0
2
Name
Order
Citations
PageRank
J. Heintz116219.20
R. Wüthrich237.48