{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T06:10:01Z","timestamp":1747548601886,"version":"3.40.5"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[1997,4,1]],"date-time":"1997-04-01T00:00:00Z","timestamp":859852800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1997,4,1]],"date-time":"1997-04-01T00:00:00Z","timestamp":859852800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Annals of Mathematics and Artificial Intelligence"],"published-print":{"date-parts":[[1997,4]]},"DOI":"10.1023\/a:1018911907086","type":"journal-article","created":{"date-parts":[[2003,2,19]],"date-time":"2003-02-19T22:07:13Z","timestamp":1045692433000},"page":"319-334","source":"Crossref","is-referenced-by-count":4,"title":["Heuristic search and pruning in polynomial constraints satisfaction"],"prefix":"10.1007","volume":"19","author":[{"given":"Hoon","family":"Hong","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"325419_CR1","unstructured":"D.S. Arnon, Algorithms for the geometry of semi-algehraic sets, Ph.D. Thesis, Technical Report 436, Computer Sciences Dept., Univ. of Wisconsin-Madison (1981)."},{"issue":"1","key":"325419_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) (1988) 267\u2013274.","journal-title":"Journal of Symbolic Computation"},{"issue":"1","key":"325419_CR3","doi-asserted-by":"publisher","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) (1988) 189\u2013212.","journal-title":"Journal of Symbolic Computation"},{"issue":"2","key":"325419_CR4","doi-asserted-by":"publisher","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) (1986) 251\u2013264.","journal-title":"J. Comput. System Sci."},{"key":"325419_CR5","series-title":"Technical Report","volume-title":"Speeding-up quantifier elimination by Groebner bases","author":"B. Buchberger","year":"1991","unstructured":"B. Buchberger and H. Hong, Speeding-up quantifier elimination by Groebner bases, Technical Report 91\u201306.0, Research Institute for Symbolic Computation, Johannes Kepler University A-4040 Linz, Austria (1991)."},{"key":"325419_CR6","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 (1988) pp. 460\u2013467.","DOI":"10.1145\/62212.62257"},{"key":"325419_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition","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, Vol. 33 (Springer-Verlag, Berlin, 1975) pp. 134\u2013183."},{"issue":"3","key":"325419_CR8","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) (September 1991) 299\u2013328.","journal-title":"Journal of Symbolic Computation"},{"key":"325419_CR9","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":"325419_CR10","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":"1","key":"325419_CR11","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1016\/S0747-7171(88)80005-1","volume":"5","author":"D. 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) (1988) 37\u201364.","journal-title":"Journal of Symbolic Computation"},{"key":"325419_CR12","unstructured":"J. Heintz, M.-F. Roy and P. Solern\u00f3, On the complexity of semialgebraic sets, in: Proc. IFIP (1989) pp. 293\u2013298."},{"key":"325419_CR13","doi-asserted-by":"crossref","unstructured":"H. Hong, An improvement of the projection operator in cylindrical algebraic decomposition, in: International Symposium of Symbolic and Algebraic Computation ISSAC-90 (1990) pp. 261\u2013264.","DOI":"10.1145\/96877.96943"},{"key":"325419_CR14","unstructured":"H. Hong, Improvements in CAD-based quantifier elimination, Ph.D. Thesis, The Ohio State University (1990)."},{"key":"325419_CR15","series-title":"Technical Report","volume-title":"Comparison of several decision algorithms for the existential theory of the reals","author":"H. Hong","year":"1991","unstructured":"H. Hong, Comparison of several decision algorithms for the existential theory of the reals, Technical Report 91\u201341.0, Research Institute for Symbolic Computation, Johannes Kepler University A-4040 Linz, Austria (1991)."},{"key":"325419_CR16","doi-asserted-by":"crossref","unstructured":"H. Hong, Simple solution formula construction in cylindrical algebraic decomposition based quantifier elimination, in: International Conference on Symbolic and Algebraic Computation ISSAC-92 (1992) pp. 177\u2013188.","DOI":"10.1145\/143242.143306"},{"key":"325419_CR17","doi-asserted-by":"crossref","unstructured":"H. Hong, Parallelization of quantifier elimination on a workstation network, in: Proceedings of AAECC 10 (Puerto Rico) (1993).","DOI":"10.1007\/3-540-56686-4_42"},{"key":"325419_CR18","doi-asserted-by":"crossref","unstructured":"H. Hong, Quantifier elimination for formulas constrained by quadratic equations, in: International Conference on Symbolic and Algebraic Computation ISSAC-93, Kiev (ACM, July 1993).","DOI":"10.1145\/164081.164140"},{"key":"325419_CR19","doi-asserted-by":"crossref","unstructured":"H. Hong, Quantifier elimination for formulas constrained by quadratic equations via slope resultants, The Computer Journal 36(5) (1993).","DOI":"10.1093\/comjnl\/36.5.439"},{"key":"325419_CR20","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":"325419_CR21","unstructured":"D. Lazard, An improved projection for cylindrical algebraic decomposition. Unpublished manuscript (1990)."},{"issue":"1","key":"325419_CR22","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) (1976) 15\u201339.","journal-title":"ACM SIGSAM Bull"},{"key":"325419_CR23","unstructured":"S. McCallum, An improved projection operator for cylindrical algebraic decomposition, Ph.D. Thesis, University of Wisconsin-Madison (1984)."},{"key":"325419_CR24","series-title":"Technical Report","volume-title":"Solving polynomial strict inequalities using cylindrical algebraic decomposition","author":"S. McCallum","year":"1987","unstructured":"S. McCallum, Solving polynomial strict inequalities using cylindrical algebraic decomposition, Technical Report 87\u201325.0, RISC-LINZ, Johannes Kepler University, A-4040 Linz, Austria (1987)."},{"key":"325419_CR25","unstructured":"J. Pearl, Heuristics (Intelligent Search Strategies for Computer Problem Solving) (Addison-Wesley, 1984)."},{"key":"325419_CR26","series-title":"Technical Report","volume-title":"On the computational complexity and geometry of the first-order theory of the reals","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\u20137501 USA (July 1989)."},{"key":"325419_CR27","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, 2nd edn., 1951).","edition":"2nd edn."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1018911907086.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1018911907086\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1018911907086.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T05:30:45Z","timestamp":1747546245000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1018911907086"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,4]]},"references-count":27,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[1997,4]]}},"alternative-id":["325419"],"URL":"https:\/\/doi.org\/10.1023\/a:1018911907086","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"type":"print","value":"1012-2443"},{"type":"electronic","value":"1573-7470"}],"subject":[],"published":{"date-parts":[[1997,4]]}}}