{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,1]],"date-time":"2025-07-01T11:06:47Z","timestamp":1751368007913},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540573227"},{"type":"electronic","value":"9783540480631"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-57322-4_10","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T07:47:17Z","timestamp":1330242437000},"page":"152-165","source":"Crossref","is-referenced-by-count":2,"title":["Heuristic search strategies for Cylindrical Algebraic Decomposition"],"prefix":"10.1007","author":[{"given":"Hoon","family":"Hong","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"10_CR1","unstructured":"D. S. Arnon. Algorithms for the geometry of semi-algebraic sets. Technical Report 436, Computer Sciences Dept, Univ. of Wisconsin-Madison, 1981. Ph.D. Thesis."},{"issue":"12","key":"10_CR2","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/S0747-7171(88)80016-6","volume":"5","author":"D. S. Arnon","year":"1988","unstructured":"D. S. Arnon. A bibliography of quantifier elimination for real closed fields. Journal of Symbolic Computation, 5(1,2):267\u2013274, 1988","journal-title":"Journal of Symbolic Computation"},{"issue":"12","key":"10_CR3","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/S0747-7171(88)80012-9","volume":"5","author":"D. S. Arnon","year":"1988","unstructured":"D. S. Arnon. A cluster-based cylindrical algebraic decomposition algorithm. Journal of Symbolic Computation, 5(1,2):189\u2013212, 1988.","journal-title":"Journal of Symbolic Computation"},{"key":"10_CR4","doi-asserted-by":"crossref","first-page":"865","DOI":"10.1137\/0213054","volume":"13","author":"D. S. Arnon","year":"1984","unstructured":"D. S. Arnon, G. E. Collins, and S. McCallum. Cylindrical algebraic decomposition I: The basic algorithm. SIAM J. Comp., 13:865\u2013877, 1984.","journal-title":"SIAM J. Comp."},{"issue":"2","key":"10_CR5","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1016\/0022-0000(86)90029-2","volume":"32","author":"M. Ben-Or","year":"1986","unstructured":"M. Ben-Or, D. Kozen, and J. H. Reif. The complexity of elementary algebra and geometry. J. Comput. System Sci., 32(2):251\u2013264, 1986.","journal-title":"J. Comput. System Sci."},{"key":"10_CR6","unstructured":"W. B\u00f6ge. Decision procedures and quantifier elimination for elementary real algebra and parametric polynomial nonlinear optimization. Manuscript in preparation, 1980."},{"key":"10_CR7","volume-title":"Technical Report 91-06.0","author":"B. Buchberger","year":"1991","unstructured":"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."},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"J. Canny. Some algebraic and geometric computations in PSPACE. In Proceedings of the 20th annual ACM symposium on the theory of computing, pages 460\u2013467, 1988.","DOI":"10.1145\/62212.62257"},{"key":"10_CR9","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1002\/cpa.3160220202","volume":"22","author":"P. J. Cohen","year":"1969","unstructured":"P. J. Cohen. Decision procedures for real and p-adic fields. Comm. Pure and Applied Math., 22:131\u2013151, 1969.","journal-title":"Comm. Pure and Applied Math."},{"key":"10_CR10","first-page":"134","volume-title":"Lecture Notes In Computer Science","author":"G. E. Collins","year":"1975","unstructured":"G. E. Collins. Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. In Lecture Notes In Computer Science, pages 134\u2013183. Springer-Verlag, Berlin, 1975. Vol. 33."},{"issue":"3","key":"10_CR11","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1016\/S0747-7171(08)80152-6","volume":"12","author":"G. E. Collins","year":"1991","unstructured":"G. E. Collins and H. Hong. Partial cylindrical algebraic decomposition for quantifier elimination. Journal of Symbolic Computation, 12(3):299\u2013328, September 1991.","journal-title":"Journal of Symbolic Computation"},{"key":"10_CR12","unstructured":"G. E. Collins and R. Loos. The SAC-2 Computer Algebra System. Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria A-4040."},{"key":"10_CR13","unstructured":"N. Fitchas, A. Galligo, and J. Morgenstern. Algorithmes repides en s\u00e9quential et en parallele pour l'\u00e9limination de quantificateurs en g\u00e9om\u00e9trie \u00e9l\u00e9mentaire. Technical report, UER de Math\u00e9matiques Universite de Paris VII, 1987. To appear in: S\u00e9minaire Structures Alg\u00e9briques Ordonn\u00e9es."},{"issue":"12","key":"10_CR14","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1016\/S0747-7171(88)80006-3","volume":"5","author":"D. Y. Grigor'ev","year":"1988","unstructured":"D. Yu. Grigor'ev. The complexity of deciding Tarski algebra. Journal of Symbolic Computation, 5(1,2):65\u2013108, 1988.","journal-title":"Journal of Symbolic Computation"},{"issue":"12","key":"10_CR15","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1016\/S0747-7171(88)80005-1","volume":"5","author":"D. Y. Grigor'ev","year":"1988","unstructured":"D. Yu. Grigor'ev and N. N. Vorobjov (Jr). Solving systems of polynomial inequalities in subexponential time. Journal of Symbolic Computation, 5(1,2):37\u201364, 1988.","journal-title":"Journal of Symbolic Computation"},{"key":"10_CR16","unstructured":"J. Heintz, M-F. Roy, and P. Solern\u00f3. On the complexity of semialgebraic sets. In Proc. IFIP, pages 293\u2013298, 1989."},{"key":"10_CR17","unstructured":"C. Holthusen. Vereinfachungen f\u00fcr Tarski's Entscheidungsverfahren der elementaren reellen Algebra. PhD thesis, University of Heidelberg, January 1974."},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1145\/96877.96943"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"H. Hong. An improvement of the projection op\u00e9rator in cylindrical algebraic decomposition. In International Symposium of Symbolic and Algebraic Computation, pages 261\u2013264, 1990.","DOI":"10.1145\/96877.96943"},{"key":"10_CR20","unstructured":"H. Hong. Improvements in CAD-based Quantifier Elimination. PhD thesis, The Ohio State University, 1990."},{"key":"10_CR21","volume-title":"Technical Report 91-41.0","author":"H. Hong","year":"1991","unstructured":"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. Submitted to Journal of Symbolic Computation."},{"key":"10_CR22","volume-title":"Technical Report 91-55.0","author":"H. Hong","year":"1991","unstructured":"H. Hong. Parallelization of quantifier elimination on workstation network. Technical Report 91-55.0, Research Institute for Symbolic Computation, Johannes Kepler University A-4040 Linz, Austria, 1991."},{"key":"10_CR23","volume-title":"Technical Report 92-02.0","author":"H. Hong","year":"1992","unstructured":"H. Hong. Simple solution formula construction in cylindrical algebraic decomposition based quantifier elimination. Technical Report 92-02.0, Research Institute for Symbolic Computation, Johannes Kepler University A-4040 Linz, Austria, 1992. To appear in International Conference on Symbolic and Algebraic Computation ISSAC-92."},{"key":"10_CR24","unstructured":"J. R. Johnson. Algorithms for Polynomial Real Root Isolation. PhD thesis, The Ohio State University, 1991."},{"key":"10_CR25","unstructured":"L. Langemyr. The cylindrical algebraic decomposition algorithm and multiple algebraic extensions. In Proc. 9th IMA Conference on the Mathematics of Surfaces, September 1990."},{"key":"10_CR26","unstructured":"D. Lazard. An improved projection for cylindrical algebraic decomposition. Unpublished manuscript, 1990."},{"issue":"1","key":"10_CR27","first-page":"15","volume":"10","author":"R. G. K. Loos","year":"1976","unstructured":"R. G. K. Loos. The algorithm description language ALDES (Report). ACM SIGSAM Bull., 10(1):15\u201339, 1976.","journal-title":"ACM SIGSAM Bull."},{"key":"10_CR28","unstructured":"S. McCallum. An Improved Projection Operator for Cylindrical Algebraic Decomposition. PhD thesis, University of Wisconsin-Madison, 1984."},{"key":"10_CR29","unstructured":"J. Pearl. Hueristics (Intelligent Search Strategies for Computer Problem Solving). Addison-Wesley, 1984."},{"key":"10_CR30","volume-title":"Technical Report 853","author":"J. Renegar","year":"1989","unstructured":"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."},{"key":"10_CR31","volume-title":"Technical Report 854","author":"J. Renegar","year":"1989","unstructured":"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."},{"key":"10_CR32","volume-title":"Technical Report 856","author":"J. Renegar","year":"1989","unstructured":"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."},{"key":"10_CR33","doi-asserted-by":"crossref","first-page":"365","DOI":"10.2307\/1969640","volume":"60","author":"A. Seidenberg","year":"1954","unstructured":"A. Seidenberg. A new decision method for elementary algebra. Ann. of Math, 60:365\u2013374, 1954.","journal-title":"Ann. of Math"},{"key":"10_CR34","doi-asserted-by":"crossref","DOI":"10.1525\/9780520348097","volume-title":"A Decision Method for Elementary Algebra and Geometry","author":"A. Tarski","year":"1951","unstructured":"A. Tarski. A Decision Method for Elementary Algebra and Geometry. Univ. of California Press, Berkeley, second edition, 1951.","edition":"second edition"}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence and Symbolic Mathematical Computing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-57322-4_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T14:31:54Z","timestamp":1687271514000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57322-4_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540573227","9783540480631"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/3-540-57322-4_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}