Scott McCallum
ABSTRACT
Collins [4] observed that quantifier elimination problems often have equational constraints, and he asserted that such constraints can be used to reduce the projection sets required for cylindrical algebraic decomposition (cad) based quantifier elimination. This paper follows on from [11], and validates the use of a semi-restricted equational projection scheme throughout the projection phase of cad. The fully restricted projection scheme as originally proposed in [4] is proved valid for four variable problems under certain conditions.
- 1.ACHIESER, N. I. Theory of Approximation. Ungar, New York, 1956.Google Scholar
- 2.ARNON, D. S., COLLINS, G. E., AND MCCALLUM, S. Cylindrical algebraic decomposition i: The basic algorithm. SIAM Journal on Computing 13 (1984), 865-877. Google ScholarDigital Library
- 3.COLLINS, G. E. Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In Proceedings of 2rid GI Conference on Automata Theory and Formal Languages, Lecture Notes in Computer Science 33 (Berlin, 1975), Springer-Verlag, pp. 134-183. Google ScholarDigital Library
- 4.COLLINS, G. E. Quantifier elimination by cylindrical algebraic decomposition - twenty years of progress. In Quantifier Elimination and Cylindrical Algebraic Decomposition (Vienna, 1998), B. F. Caviness and J. R. Johnson, Eds., Springer-Verlag, pp. 8-23.Google Scholar
- 5.COLLINS, G. E., AND HONO, H. Partial cylindrical algebraic decomposition for quantifier elimination. Journal of Symbolic Computation 12 (1991), 299-328. Google ScholarDigital Library
- 6.KAPLAN, W. Introduction to Analytic Functions. Addison-Wesley, Reading, 1966.Google Scholar
- 7.Loos, R. Computing in algebraic extensions. In Computing, Supplementum 4 (Vienna, 1982), Springer-Verlag, pp. 173-187.Google Scholar
- 8.MCCALLUM, S. An Improved Projection Operation for Cylindrical Algebraic Decomposition. PhD thesis, University of Wisconsin-Madison, 1984. Google ScholarDigital Library
- 9.MCCALLUM, S. An improved projection operation for cylindrical algebraic decomposition of three-dimensional space. Journal of Symbolic Computation 5 (1988), 141-161. Google ScholarDigital Library
- 10.McCALLUM, S. An improved projection operation for cylindrical algebraic decomposition. In Quantifier Elimination and Cylindrical Algebraic Decomposition (Vienna, 1998), B. F. Caviness and J. R. Johnson, Eds., Springer-Verlag, pp. 242-268. 230Google Scholar
- 11.MCCALLUM, S. On projection in cad-based quantifier elimination with equational constraint. In Proceedings of the 1999 International Symposium on Symbolic and Algebraic Computation (New York, 1999), S. Dooley, Ed., ACM Press, pp. 145-149. Google ScholarDigital Library
- 12.WALKER, R. J. Algebraic Curves. Springer-Verlag, New York, 1978.Google Scholar
Index Terms
- On propagation of equational constraints in CAD-based quantifier elimination
Recommendations
On delineability of varieties in CAD-based quantifier elimination with two equational constraints
ISSAC '09: Proceedings of the 2009 international symposium on Symbolic and algebraic computationLet V ⊂ Rr denote the real algebraic variety defined by the conjunction f = 0 ∧ g = 0, where f and g are real polynomials in the variables x1, ..., xr and let S be a submanifold of Rr-2. This paper proposes the notion of the analytic delineability of V ...
A formal quantifier elimination for algebraically closed fields
AISC'10/MKM'10/Calculemus'10: Proceedings of the 10th ASIC and 9th MKM international conference, and 17th Calculemus conference on Intelligent computer mathematicsWe prove formally that the first order theory of algebraically closed fields enjoys quantifier elimination, and hence is decidable. This proof is organized in two modular parts. We first reify the first order theory of rings and prove that quantifier ...
Comments