{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T01:20:05Z","timestamp":1773624005538,"version":"3.50.1"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1998,8,1]],"date-time":"1998-08-01T00:00:00Z","timestamp":901929600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,8,1]],"date-time":"1998-08-01T00:00:00Z","timestamp":901929600000},"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":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[1998,8]]},"DOI":"10.1023\/a:1005983105493","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T00:10:48Z","timestamp":1040515848000},"page":"23-38","source":"Crossref","is-referenced-by-count":38,"title":["Testing Positiveness of Polynomials"],"prefix":"10.1007","volume":"21","author":[{"given":"Hoon","family":"Hong","sequence":"first","affiliation":[]},{"given":"Dalibor","family":"Jaku\u0161","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"158873_CR1","unstructured":"Arnon, D. S.: Algorithms for the Geometry of Semi-Algebraic Sets, Ph.D. thesis, Comp. Sci. Dept., Univ. of Wisconsin-Madison, 1981, Tech. Report No. 436."},{"key":"158873_CR2","doi-asserted-by":"crossref","first-page":"878","DOI":"10.1137\/0213055","volume":"13","author":"D. S. Arnon","year":"1984","unstructured":"Arnon, D. S., Collins, G. E., and McCallum, S.: Cylindrical algebraic decomposition II: An adjacency algorithm for the plane, SIAM J. Comp.\n13 (1984), 878\u2013889.","journal-title":"SIAM J. Comp."},{"key":"158873_CR3","doi-asserted-by":"crossref","unstructured":"Arnon, D. S., Collins, G. E., and McCallum, S.: An adjacency algorithm for cylindrical algebraic decompositions of three-dimensional space, Journal of Symbolic Computation\n5(1,2) (1988).","DOI":"10.1016\/S0747-7171(88)80011-7"},{"issue":"2","key":"158873_CR4","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1016\/0167-6423(87)90030-X","volume":"9","author":"A. Ben-Cherifa","year":"1987","unstructured":"Ben-Cherifa, A. and Lescanne, P.: Termination of rewriting systems by polynomial interpretations and its implementation, Science of Computer Programming\n9(2) (1987), 137\u2013159.","journal-title":"Science of Computer Programming"},{"key":"158873_CR5","unstructured":"Brown, C. and Collins, G.: Simplification of truth invariant CAD's and solution formula construction, in Proceedings of IMACS-ACA'96, 1996."},{"key":"158873_CR6","doi-asserted-by":"crossref","unstructured":"Canny, J. F.: Improved algorithms for sign and existential quantifier elimination, The Computer Journal\n36 (1993), 409\u2013418. In a special issue on computational quantifier elimination, edited by H. Hong.","DOI":"10.1093\/comjnl\/36.5.409"},{"key":"158873_CR7","first-page":"134","volume-title":"Lecture Notes In Computer Science","author":"G. E. Collins","year":"1975","unstructured":"Collins, G. E.: Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition, in Lecture Notes In Computer Science 33, Springer-Verlag, Berlin, 1975, pp. 134\u2013183."},{"key":"158873_CR8","unstructured":"Collins, G. E.: Quantifier elimination by cylindrical algebraic decomposition - 20 years of progress, in B. Caviness and J. Johnson (eds), Quantifier Elimination and Cylindrical Algebraic Decomposition, Texts and Monographs in Symbolic Computation, Springer-Verlag, 1994, to appear."},{"issue":"3","key":"158873_CR9","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1016\/S0747-7171(08)80152-6","volume":"12","author":"G. E. Collins","year":"1991","unstructured":"Collins, G. E. and Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination, Journal of Symbolic Computation\n12(3) (1991), 299\u2013328.","journal-title":"Journal of Symbolic Computation"},{"key":"158873_CR10","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"Dershowitz, N.: Termination of rewriting, Journal of Symbolic Computation\n3 (1987), 69\u2013116.","journal-title":"Journal of Symbolic Computation"},{"key":"158873_CR11","doi-asserted-by":"crossref","unstructured":"Giesl, J.: Generating polynomial orderings for termination proofs, in Proceedings of the 6th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science 914, Springer-Verlag, 1995.","DOI":"10.1007\/3-540-59200-8_77"},{"key":"158873_CR12","unstructured":"Gonz\u00e1lez-Vega, L.: A combinatorial algorithm solving some quantifier elimination problems, in Quantifier Elimination and Cylindrical Algebraic Decomposition, Springer-Verlag, 1996."},{"issue":"12","key":"158873_CR13","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":"Grigor'ev, D. Yu.: The complexity of deciding Tarski algebra, Journal of Symbolic Computation\n5(1,2) (1988), 65\u2013108.","journal-title":"Journal of Symbolic Computation"},{"key":"158873_CR14","unstructured":"Heintz, J., Roy, M.-F., and Solern\u00f3, P.: On the complexity of semialgebraic sets, in G. X. Ritter (ed.), Proc. IFIP, North-Holland, 1989, pp. 293\u2013298."},{"key":"158873_CR15","doi-asserted-by":"crossref","unstructured":"Hong, H.: An improvement of the projection operator in cylindrical algebraic decomposition, in International Symposium of Symbolic and Algebraic Computation (ISSAC-90), ACM, 1990, pp. 261\u2013264.","DOI":"10.1145\/96877.96943"},{"key":"158873_CR16","unstructured":"Hong, H.: Improvements in CAD-based Quantifier Elimination, Ph.D. thesis, The Ohio State University, 1990."},{"key":"158873_CR17","doi-asserted-by":"crossref","unstructured":"Hong, H.: 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":"158873_CR18","doi-asserted-by":"crossref","unstructured":"Hong, H.: Parallelization of quantifier elimination on a workstation network, in G. Cohen, T. Mora, and O. Moreno (eds), AAECC-10, Lecture Notes in Computer Science 673, Springer-Verlag, 1993, pp. 170\u2013179.","DOI":"10.1007\/3-540-56686-4_42"},{"issue":"5","key":"158873_CR19","first-page":"440","volume":"36","author":"H. Hong","year":"1993","unstructured":"Hong, H.: Quantifier elimination for formulas constrained by quadratic equations via slope resultants, The Computer Journal\n36(5) (1993), 440\u2013449.","journal-title":"The Computer Journal"},{"key":"158873_CR20","unstructured":"Hong, H.: Approximate quantifier elimination, in Proceedings of SCAN'95, 1995. Invited talk."},{"key":"158873_CR21","unstructured":"Hong, H.: Generic quantifier elimination, in Proceedings of IMACS-ACA'95, 1995."},{"issue":"34","key":"158873_CR22","first-page":"319","volume":"19","author":"H. Hong","year":"1997","unstructured":"Hong, H.: Heuristic search and pruning in polynomial constraints satisfaction, Annals of Math. and AI\n19(3,4) (1997), 319\u2013334.","journal-title":"Annals of Math. and AI"},{"key":"158873_CR23","unstructured":"Hong, H. and Neubacher, A.: Approximate quantifier elimination, in Proceedings of IMACS-ACA'96, 1996."},{"key":"158873_CR24","volume-title":"A finite termination algorithm","author":"D. Lankford","year":"1976","unstructured":"Lankford, D.: A finite termination algorithm, Technical report, Southwestern University, Georgetown, Texas, 1976."},{"issue":"5","key":"158873_CR25","doi-asserted-by":"crossref","first-page":"450","DOI":"10.1093\/comjnl\/36.5.450","volume":"36","author":"R. Loos","year":"1993","unstructured":"Loos, R. and Weispfenning, V.: Applying linear quantifier elimination, Computer Journal\n36(5) (1993), 450\u2013462.","journal-title":"Computer Journal"},{"key":"158873_CR26","unstructured":"McCallum, S.: An Improved Projection Operator for Cylindrical Algebraic Decomposition, Ph.D. thesis, University of Wisconsin-Madison, 1984."},{"key":"158873_CR27","doi-asserted-by":"crossref","unstructured":"McCallum, S.: An improved projection operator for cylindrical algebraic decomposition, Journal of Symbolic Computation\n5(1,2) (1988).","DOI":"10.1016\/S0747-7171(88)80010-5"},{"key":"158873_CR28","doi-asserted-by":"crossref","unstructured":"McCallum, S.: Solving polynomial strict inequalities using cylindrical algebraic decomposition, The Computer Journal\n36(5) (1993), 432\u2013438. In a special issue on computational quantifier elimination, edited by H. Hong.","DOI":"10.1093\/comjnl\/36.5.432"},{"issue":"3","key":"158873_CR29","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1016\/S0747-7171(10)80003-3","volume":"13","author":"J. Renegar","year":"1992","unstructured":"Renegar, J.: On the computational complexity and geometry of the first-order theory of the reals, Journal of Symbolic Computation\n13(3) (1992), 255\u2013300.","journal-title":"Journal of Symbolic Computation"},{"key":"158873_CR30","doi-asserted-by":"crossref","unstructured":"Saunders, B. D., Lee, H. R., and Abdali, S. K.: A parallel implementation of the cylindrical algebraic decomposition algorithm, in International Symposium of Symbolic and Algebraic Computation, 1990, pp. 298\u2013307.","DOI":"10.1145\/74540.74576"},{"key":"158873_CR31","doi-asserted-by":"crossref","unstructured":"Steinbach, J.: Proving polynomials positive, in Proceedings of the 12th FST&TCS, Lecture Notes in Computer Science 652, New Delhi, India, 1992.","DOI":"10.1007\/3-540-56287-7_105"},{"key":"158873_CR32","unstructured":"Steinbach, J.: Termination of Rewriting, Ph.D. thesis, 1994."},{"key":"158873_CR33","unstructured":"Tarski, A.: The completeness of elementary algebra and geometry, 1930. Reprinted in 1967."},{"key":"158873_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":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry, 2nd edn, Univ. of California Press, Berkeley, 1951.","edition":"2nd edn"},{"issue":"12","key":"158873_CR35","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0747-7171(88)80003-8","volume":"5","author":"V. Weispfenning","year":"1988","unstructured":"Weispfenning, V.: The complexity of linear problems in fields, Journal of Symbolic Computation\n5(1,2) (1988), 3\u201327.","journal-title":"Journal of Symbolic Computation"},{"key":"158873_CR36","doi-asserted-by":"crossref","unstructured":"Weispfenning, V.: Quantifier elimination for real algebra - the cubic case, in ISSAC-94, 1994, pp. 258\u2013263.","DOI":"10.1145\/190347.190425"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005983105493.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1005983105493\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005983105493.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:25:20Z","timestamp":1749122720000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1005983105493"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,8]]},"references-count":36,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1998,8]]}},"alternative-id":["158873"],"URL":"https:\/\/doi.org\/10.1023\/a:1005983105493","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998,8]]}}}