Simple solution formula construction in cylindrical algebraic decomposition based quantifier elimination

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	N. I. Achieser. Theory of Approximation. Frederick Ungar Publishing Co., New York, 1956.
	2	Dennis Soule Arnon, Algorithms for the geometry of semi-algebraic sets, 1981
	3	Dennis S. Arnon, A cluster-based cylindrical algebraic decomposition algorithm, Journal of Symbolic Computation, v.5 n.1-2, p.189-212, February/April 1988 [doi>10.1016/S0747-7171(88)80012-9]
	4	Dennis S. Arnon , George E. Collins , Scott McCallum, Cylindrical algebraic decomposition I: the basic algorithm, SIAM Journal on Computing, v.13 n.4, p.865-877, Nov. 1984 [doi>10.1137/0213054]
	5	Dennis S. Arnon , Maurice Mignotte, On mechanical quantifier elimination for elementary algebra and geometry, Journal of Symbolic Computation, v.5 n.1-2, p.237-259, February/April 1988 [doi>10.1016/S0747-7171(88)80014-2]
	6	Dennis S. Arnon , Scott F. Smith, Towards mechanical solution of the Kahan Ellipse Problem 1, Proceedings of the European Computer Algebra Conference on Computer Algebra, p.36-44, March 28-30, 1983
	7	M. Bartholomeus and H. D. Man. Presto-II: Yet another logic minimizer for programmed logic arrays. In Proc. Int. Syrup. Circ. Syst., June 1985.
	8	Michael Ben-Or , Dexter Kozen , John Reif, The complexity of elementary algebra and geometry, Journal of Computer and System Sciences, v.32 n.2, p.251-264, April 1986 [doi>10.1016/0022-0000(86)90029-2]
	9	W. BSge. Decision procedures and quantifier elimination for elementary real algebra and parametric polynomial nonlinear optimization. Manuscript in preparation, 1980.
	10	Robert King Brayton , Alberto L. Sangiovanni-Vincentelli , Curtis T. McMullen , Gary D. Hachtel, Logic Minimization Algorithms for VLSI Synthesis, Kluwer Academic Publishers, Norwell, MA, 1984
	11	B. Buchberger. An Algorithm for Finding a Basis for the Residue Class Ring of a Zero-Dimensional Polynomial Ideal. PhD thesis, Universitat Innsbruck, Institut fur Mathematik, 1965. German.
	12	B. Buchberger and H. Hong. Speeding-up quantifier elimination by Groebner bases. Technical Report 91-06.0, Research Institute for Symbolic Computation, Johannes Kepler University A-4040 Linz, Austria, 1991.
	13	John Canny, Some algebraic and geometric computations in PSPACE, Proceedings of the twentieth annual ACM symposium on Theory of computing, p.460-469, May 02-04, 1988, Chicago, Illinois, United States [doi>10.1145/62212.62257]
	14	P. J. Cohen. Decision procedures for real and p-aclic fields. Comm. Pzt,e and Applied Ma~h., 22:131-15I, 1969.
	15	George E. Collins, Hauptvortrag: Quantifier elimination for real closed fields by cylindrical algebraic decomposition, Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages, p.134-183, May 20-23, 1975
	16	George E. Collins , Hoon Hong, Partial cylindrical algebraic decomposition for quantifier elimination, Journal of Symbolic Computation, v.12 n.3, p.299-328, Sept. 1991 [doi>10.1016/S0747-7171(08)80152-6]
	17	G. E. Collins , J. R. Johnson, Quantifier elimination and the sign variation method for real root isolation, Proceedings of the ACM-SIGSAM 1989 international symposium on Symbolic and algebraic computation, p.264-271, July 17-19, 1989, Portland, Oregon, United States [doi>10.1145/74540.74574]
	18	G. E. Collins and R. Loos. The SAC-2 Compu.. tar Algebra System. Department of Computer and Information Sciences, Ohio State University.
	19	C. Delzell. A continuous, constructive solution to hilbert's 17th problem. Invent. math., 76"365-384, 1984.
	20	N. Fitchas, A. Galligo, and J. Morgenstern. Algorithmes repides en sdquential et en par-. allele pour l'61imination de quantificateurs e n g6om6trie 616mentaire. Technical report, UER cle Math6matiques Universite de Paris VII, 1987. To appear in' S6minaire Structures Alg6briques Or-. donndes.
	21	M. R. Garey and D. S. Johnson. Computers and Intractability. W. H. Freeman and Company, 1979..
	22	D. Yu. Grigor'ev, Complexity of deciding Tarski algebra, Journal of Symbolic Computation, v.5 n.1-2, p.65-108, February/April 1988 [doi>10.1016/S0747-7171(88)80006-3]
	23	D. Yu. Grigor'ev , N. N. Vorobjov, Solving systems of polynomial inequalities in subexponential time, Journal of Symbolic Computation, v.5 n.1-2, p.37-64, February/April 1988 [doi>10.1016/S0747-7171(88)80005-1]
	24	J. Heintz, M-F. Roy, and P. Solern6. On the cornplexity of semialgebraic sets. In Proc. IFIP, pages 293-298, 1989.
	25	F. E. Hohn. Applied Boolean Algebra. The Macmillan Company, New York, second edition, 1966.
	26	C. Holthusen. Vereinfachungen fiir Tarski's Entscheidungsverfahven der elementaven veellen Algebra. PhD thesis, University of Heidelberg, January 1974.
	27	H. Hong. An improvement of the projection operator in cylindrical algebraic decomposition. Technical Report OSU-CISRC-12/89 TR55, Computer Science Dept, The Ohio State University, 1989.
	28	H. Hong, An improvement of the projection operator in cylindrical algebraic decomposition, Proceedings of the international symposium on Symbolic and algebraic computation, p.261-264, August 20-24, 1990, Tokyo, Japan [doi>10.1145/96877.96943]
	29	Hoon Hong , George E. Collins, Improvements in cad-based quantifier elimination, 1990
	30	H. Hong. Collision problems by partial CAD construction. Technical report, Research Institute for Symbolic Computation, Johannes Kepler University A-4040 Linz, Austria, January 199i.
	31	H. Hong. Comparison of several decision algorithms for the existential theory of the reals. Technical Report 91-41.0, Research Institute for Symbolic Computation, Johannes Kepler University A- 4040 Linz, Austria, 1991.
	32	H. Hong. ParaIlelization of quantifier elimination on workstation network. Technical Report 91-55.0, Research Institute for Symbolic Computation, Johannes Kepler University A-4040 Linz, Austria, 1991.
	33	S. J. Hong, R. G. Cain, and D. L. Ostapko. Mini: A heuristic approach for logic minimization. IBM Journal of Research and Development, pages 443- 458, 1974. Sep.
	34	Jeremy R. Johnson, Algorithms for polynomial real root isolation, Ohio State University, Columbus, OH, 1992
	35	W. Kahan, Problem #9: an ellipse problem, ACM SIGSAM Bulletin, v.9 n.3, p.11-12, August 1975 [doi>10.1145/1088309.1088312]
	36	Lars Langemyr, Algorithms for a Multiple Algebraic Extension II, Proceedings of the 9th International Symposium, on Applied Algebra, Algebraic Algorithms and Error-Correcting Codes, p.224-233, October 07-11, 1991
	37	Markus Lauer, A solution to Kahan's problem (SIGSAM problem no. 9), ACM SIGSAM Bulletin, v.11 n.2, p.16-20, May 1977 [doi>10.1145/1088240.1088244]
	38	Daniel Lazard, Quantifier elimination: optimal solution for two classical examples, Journal of Symbolic Computation, v.5 n.1-2, p.261-266, February/April 1988 [doi>10.1016/S0747-7171(88)80015-4]
	39	D. Lazard. An improved projection for cylindrical algebraic decomposition. Unpublished manuscript, 1990.
	40	Rüdiger G. K. Loos, The algorithm description language ALDES (report), ACM SIGSAM Bulletin, v.10 n.1, p.14-38, February 1976 [doi>10.1145/1093390.1093395]
	41	Scott McCallum, An improved projection operation for cylindrical algebraic decomposition (computer algebra, geometry, algorithms), 1984
	42	E. J. McCluskev. Minimization of boolean fi,nctions. Bell System "l'r.~b,i,',sl .1,, ,i ~ , ,,1. :V,'I t i 7 1444, 1956.
	43	Mignotte. Computer versus paper and pencil. In Proc. CALSYF, pages 63-69, 1986. Vo. 4.
	44	W. V. O. Quine. The problem of simplifying truth functions. American Mathemat2cal Mo~tb.ly, 59:521-531, 1952. Nov.
	45	W. V. O. Quine. A way to simplify truth functions. American Mathematical Monthly, 62:627- 631, 1955. Nov.
	46	W. V. O. Quine. On cores and prime implicants of truth functions. American Mathematical Monthly, 66:755-760, 1959. Nov.
	47	J. Renegar. On the computational complexity and geometry of the first-order theory of the reals (part I). Technical Report 853, Cornell University, Ithaca, New York 14853-7501 USA, July 1989.
	48	J. Renegar. On the computational complexity and geometry of the first-order theory of the reals (part II). Technical Report 854, Cornell University~ ithaca, New York 14853-7501 USA~ July 1989.
	49	J. Renegar. On the computational complexity and geometry of the first-order theory of the reals (part III). Technical Report 856, Cornell University, Ithaca, New York 14853-7501 USA, August 1989.
	50	R. Rudell. Multiple-Valued Logic Minimization for PLA Synthesis. Technical Report UCB/ERL M86/65, University of California, Berkeley, USA, 1986.
	51	T. Sasao. Comparison of minimization algorithms for multiple-valued expressons. In Proc. 12 ~h In~. Syrup. on Mul~. Val. Logic, 1982.
	52	A. Seidenberg. A new decision method for elementary algebra. Ann. of Ma$h, 60:365-374, 1954.
	53	P. Simanyi. Pop reference manual. Technical report, University of California, Berkeley, September 1983.
	54	A. Tarski. A Decision Me~hod for Elementary Algebra and GeomeSry. Univ. of California Press, Berkeley, second edition, 1951.