{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T20:23:07Z","timestamp":1743020587562,"version":"3.40.3"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319986531"},{"type":"electronic","value":"9783319986548"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-99639-4_17","type":"book-chapter","created":{"date-parts":[[2018,8,22]],"date-time":"2018-08-22T15:43:34Z","timestamp":1534952614000},"page":"238-253","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Positive Solutions of Systems of Signed Parametric Polynomial Inequalities"],"prefix":"10.1007","author":[{"given":"Hoon","family":"Hong","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8088-340X","authenticated-orcid":false,"given":"Thomas","family":"Sturm","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,8,23]]},"reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-319-42547-4_3","volume-title":"Intelligent Computer Mathematics","author":"E \u00c1brah\u00e1m","year":"2016","unstructured":"\u00c1brah\u00e1m, E.: $${\\sf SC}^{\\sf 2} $$ : satisfiability checking meets symbolic computation. In: Kohlhase, M., Johansson, M., Miller, B., de Moura, L., Tompa, F. (eds.) CICM 2016. LNCS (LNAI), vol. 9791, pp. 28\u201343. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-42547-4_3"},{"key":"17_CR2","unstructured":"Arnon, D.S.: Algorithms for the geometry of semi-algebraic sets. Ph.D. thesis. Technical report 436, Computer Science Department, University of Wisconsin-Madison (1981)"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"17_CR4","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: version 2.6. Technical report, Department of Computer Science, The University of Iowa (2017)"},{"issue":"6","key":"17_CR5","doi-asserted-by":"publisher","first-page":"1002","DOI":"10.1145\/235809.235813","volume":"43","author":"S Basu","year":"1996","unstructured":"Basu, S., Pollack, R., Roy, M.F.: On the combinatorial and algebraic complexity of quantifier elimination. JACM 43(6), 1002\u20131045 (1996). https:\/\/doi.org\/10.1145\/235809.235813","journal-title":"JACM"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-02959-2_12","volume-title":"Automated Deduction \u2013 CADE-22","author":"T Bouton","year":"2009","unstructured":"Bouton, T., Caminha B. de Oliveira, D., D\u00e9harbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 151\u2013156. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_12"},{"key":"17_CR7","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1145\/3087604.3087622","volume-title":"Proceedings of the ISSAC 2017","author":"R Bradford","year":"2017","unstructured":"Bradford, R.: A case study on the parametric occurrence of multiple steady states. In: Burr, M. (ed.) Proceedings of the ISSAC 2017, pp. 45\u201352. ACM, New York (2017). https:\/\/doi.org\/10.1145\/3087604.3087622"},{"key":"17_CR8","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1145\/345542.345575","volume-title":"Proceedings of the ISSAC 2000","author":"CW Brown","year":"2000","unstructured":"Brown, C.W.: Improved projection for CAD\u2019s of $$\\mathbb{R}^3$$ . In: Traverso, C. (ed.) Proceedings of the ISSAC 2000, pp. 48\u201353. ACM, New York (2000). https:\/\/doi.org\/10.1145\/345542.345575"},{"issue":"4","key":"17_CR9","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/968708.968710","volume":"37","author":"CW Brown","year":"2003","unstructured":"Brown, C.W.: QEPCAD B: a program for computing with semi-algebraic sets using CADs. ACM SIGSAM Bull. 37(4), 97\u2013108 (2003). https:\/\/doi.org\/10.1145\/968708.968710","journal-title":"ACM SIGSAM Bull."},{"key":"17_CR10","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1145\/62212.62257","volume-title":"Proceedings of the STOC 1988","author":"J Canny","year":"1988","unstructured":"Canny, J.: Some algebraic and geometric computations in PSPACE. In: Simon, J. (ed.) Proceedings of the STOC 1988, pp. 460\u2013467. ACM, New York (1988). https:\/\/doi.org\/10.1145\/62212.62257"},{"key":"17_CR11","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.jsc.2011.12.014","volume":"49","author":"C Chen","year":"2013","unstructured":"Chen, C., Davenport, J.H., May, J.P., Moreno Maza, M., Xia, B., Xiao, R.: Triangular decomposition of semi-algebraic systems. J. Symb. Comput. 49, 3\u201326 (2013). https:\/\/doi.org\/10.1016\/j.jsc.2011.12.014","journal-title":"J. Symb. Comput."},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93\u2013107. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7"},{"issue":"3","key":"17_CR13","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1016\/S0747-7171(08)80152-6","volume":"12","author":"GE Collins","year":"1991","unstructured":"Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput. 12(3), 299\u2013328 (1991). https:\/\/doi.org\/10.1016\/S0747-7171(08)80152-6","journal-title":"J. Symb. Comput."},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Automata Theory and Formal Languages 2nd GI Conference Kaiserslautern, May 20\u201323, 1975","author":"GE Collins","year":"1975","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134\u2013183. Springer, Heidelberg (1975). https:\/\/doi.org\/10.1007\/3-540-07407-4_17"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/978-3-319-24318-4_26","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"F Corzilius","year":"2015","unstructured":"Corzilius, F., Kremer, G., Junges, S., Schupp, S., \u00c1brah\u00e1m, E.: SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 360\u2013368. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_26"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"17_CR17","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1145\/1005285.1005303","volume-title":"Proceedings of the ISSAC 2004","author":"A Dolzmann","year":"2004","unstructured":"Dolzmann, A., Seidl, A., Sturm, T.: Efficient projection orders for CAD. In: Gutierrez, J. (ed.) Proceedings of the ISSAC 2004, pp. 111\u2013118. ACM, New York (2004). https:\/\/doi.org\/10.1145\/1005285.1005303"},{"issue":"2","key":"17_CR18","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/261320.261324","volume":"31","author":"A Dolzmann","year":"1997","unstructured":"Dolzmann, A., Sturm, T.: REDLOG: computer algebra meets computer logic. ACM SIGSAM Bull. 31(2), 2\u20139 (1997). https:\/\/doi.org\/10.1145\/261320.261324","journal-title":"ACM SIGSAM Bull."},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices\u00a02.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49"},{"key":"17_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-319-66320-3_8","volume-title":"Computer Algebra in Scientific Computing","author":"M England","year":"2017","unstructured":"England, M., Errami, H., Grigoriev, D., Radulescu, O., Sturm, T., Weber, A.: Symbolic versus numerical computation and visualization of parameter regions for multistationarity of biological networks. In: Gerdt, V.P., Koepf, W., Seiler, W.M., Vorozhtsov, E.V. (eds.) CASC 2017. LNCS, vol. 10490, pp. 93\u2013108. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66320-3_8"},{"key":"17_CR21","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/j.jcp.2015.02.050","volume":"291","author":"H Errami","year":"2015","unstructured":"Errami, H., Eiswirth, M., Grigoriev, D., Seiler, W.M., Sturm, T., Weber, A.: Detection of Hopf bifurcations in chemical reaction networks using convex coordinates. J. Comput. Phys. 291, 279\u2013302 (2015). https:\/\/doi.org\/10.1016\/j.jcp.2015.02.050","journal-title":"J. Comput. Phys."},{"key":"17_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-319-66167-4_11","volume-title":"Frontiers of Combining Systems","author":"P Fontaine","year":"2017","unstructured":"Fontaine, P., Ogawa, M., Sturm, T., Vu, X.T.: Subtropical satisfiability. In: Dixon, C., Finger, M. (eds.) FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 189\u2013206. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66167-4_11"},{"key":"17_CR23","series-title":"Texts and Monographs in Symbolic Computation","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-7091-9459-1_19","volume-title":"Quantifier Elimination and Cylindrical Algebraic Decomposition","author":"L Gonz\u00e1lez-Vega","year":"1998","unstructured":"Gonz\u00e1lez-Vega, L.: A combinatorial algorithm solving some quantifier elimination problems. In: Caviness, B.F., Johnson, J.R. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation, pp. 365\u2013375. Springer, Vienna (1998). https:\/\/doi.org\/10.1007\/978-3-7091-9459-1_19"},{"issue":"1\u20132","key":"17_CR24","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/S0747-7171(88)80005-1","volume":"5","author":"D Grigoriev","year":"1988","unstructured":"Grigoriev, D., Vorobjov, N.: Solving systems of polynomial inequalities in subexponential time. J. Symb. Comput. 5(1\u20132), 37\u201364 (1988). https:\/\/doi.org\/10.1016\/S0747-7171(88)80005-1","journal-title":"J. Symb. Comput."},{"key":"17_CR25","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1145\/96877.96943","volume-title":"Proceedings of the ISSAC 1990","author":"H Hong","year":"1990","unstructured":"Hong, H.: An improvement of the projection operator in cylindrical algebraic decomposition. In: Watanabe, S., Nagata, M. (eds.) Proceedings of the ISSAC 1990, pp. 261\u2013264. ACM, New York (1990). https:\/\/doi.org\/10.1145\/96877.96943"},{"key":"17_CR26","unstructured":"Hong, H.: Improvements in CAD-based quantifier elimination. Ph.D. thesis, The Ohio State University (1990)"},{"issue":"7","key":"17_CR27","doi-asserted-by":"publisher","first-page":"883","DOI":"10.1016\/j.jsc.2011.05.014","volume":"47","author":"H Hong","year":"2012","unstructured":"Hong, H., Din, M.S.E.: Variant quantifier elimination. J. Symb. Comput. 47(7), 883\u2013901 (2012). https:\/\/doi.org\/10.1016\/j.jsc.2011.05.014","journal-title":"J. Symb. Comput."},{"key":"17_CR28","unstructured":"Ko\u0161ta, M.: New concepts for real quantifier elimination by virtual substitution. Doctoral dissertation, Saarland University, Germany (2016). https:\/\/doi.org\/10.22028\/D291-26679"},{"issue":"5","key":"17_CR29","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1093\/comjnl\/36.5.450","volume":"36","author":"R Loos","year":"1993","unstructured":"Loos, R., Weispfenning, V.: Applying linear quantifier elimination. Comput. J. 36(5), 450\u2013462 (1993). https:\/\/doi.org\/10.1093\/comjnl\/36.5.450","journal-title":"Comput. J."},{"key":"17_CR30","unstructured":"McCallum, S.: An improved projection operator for cylindrical algebraic decomposition. Ph.D. thesis, University of Wisconsin-Madison (1984)"},{"issue":"1","key":"17_CR31","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/s10208-014-9239-3","volume":"16","author":"S M\u00fcller","year":"2016","unstructured":"M\u00fcller, S., Feliu, E., Regensburger, G., Conradi, C., Shiu, A., Dickenstein, A.: Sign conditions for injectivity of generalized polynomial maps with applications to chemical reaction networks and real algebraic geometry. Found. Comput. Math. 16(1), 66\u201397 (2016). https:\/\/doi.org\/10.1007\/s10208-014-9239-3","journal-title":"Found. Comput. Math."},{"issue":"6","key":"17_CR32","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL(T). JACM 53(6), 937\u2013977 (2006). https:\/\/doi.org\/10.1145\/1217856.1217859","journal-title":"JACM"},{"issue":"3","key":"17_CR33","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1016\/S0747-7171(10)80004-5","volume":"13","author":"J Renegar","year":"1992","unstructured":"Renegar, J.: On the computational complexity and geometry of the first-order theory of the reals. Part II: the general decision problem. Preliminaries for quantifier elimination. J. Symb. Comput. 13(3), 301\u2013328 (1992). https:\/\/doi.org\/10.1016\/S0747-7171(10)80004-5","journal-title":"J. Symb. Comput."},{"key":"17_CR34","volume-title":"Theory of Linear and Integer Programming","author":"A Schrijver","year":"1986","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Chichester (1986)"},{"issue":"9","key":"17_CR35","doi-asserted-by":"publisher","first-page":"1021","DOI":"10.1016\/j.jsc.2006.06.004","volume":"41","author":"A Strzebonski","year":"2006","unstructured":"Strzebonski, A.: Cylindrical algebraic decomposition using validated numerics. J. Symb. Comput. 41(9), 1021\u20131038 (2006). https:\/\/doi.org\/10.1016\/j.jsc.2006.06.004","journal-title":"J. Symb. Comput."},{"key":"17_CR36","unstructured":"Sturm, T.: Real quantifier elimination in geometry. Doctoral dissertation, University of Passau, Germany (1999)"},{"key":"17_CR37","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1145\/2755996.2756677","volume-title":"Proceedings of the ISSAC 2015","author":"T Sturm","year":"2015","unstructured":"Sturm, T.: Subtropical real root finding. In: Yokoyama, K., Linton, S., Robertz, D. (eds.) Proceedings of the ISSAC 2015, pp. 347\u2013354. ACM, New York (2015). https:\/\/doi.org\/10.1145\/2755996.2756677"},{"key":"17_CR38","volume-title":"The Completeness of Elementary Algebra and Geometry","author":"A Tarski","year":"1930","unstructured":"Tarski, A.: The Completeness of Elementary Algebra and Geometry. Institute Blaise Pascal, Paris (1930). Reprinted by CNRS 1967"},{"key":"17_CR39","doi-asserted-by":"crossref","unstructured":"Viro, O.: Dequantization of real algebraic geometry on logarithmic paper. CoRR arXiv:math\/0005163 (2000)","DOI":"10.1007\/978-3-0348-8268-2_8"},{"issue":"4","key":"17_CR40","doi-asserted-by":"publisher","first-page":"899","DOI":"10.1007\/s11538-010-9618-0","volume":"73","author":"A Weber","year":"2011","unstructured":"Weber, A., Sturm, T., Abdel-Rahman, E.O.: Algorithmic global criteria for excluding oscillations. Bull. Math. Biol. 73(4), 899\u2013916 (2011). https:\/\/doi.org\/10.1007\/s11538-010-9618-0","journal-title":"Bull. Math. Biol."},{"key":"17_CR41","series-title":"Texts and Monographs in Symbolic Computation","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/978-3-7091-9459-1_20","volume-title":"Quantifier Elimination and Cylindrical Algebraic Decomposition","author":"V Weispfenning","year":"1998","unstructured":"Weispfenning, V.: A new approach to quantifier elimination for real algebra. In: Caviness, B.F., Johnson, J.R. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation, pp. 376\u2013392. Springer, Vienna (1998). https:\/\/doi.org\/10.1007\/978-3-7091-9459-1_20"},{"key":"17_CR42","volume-title":"The Mathematica Book","author":"S Wolfram","year":"2003","unstructured":"Wolfram, S.: The Mathematica Book, 5th edn. Cambridge University Press, Cambridge (2003)","edition":"5"},{"key":"17_CR43","first-page":"275","volume-title":"Proceedings of the A3L 2005","author":"H Yanami","year":"2005","unstructured":"Yanami, H., Anai, H.: SyNRAC: a Maple toolbox for solving real algebraic constraints. In: Dolzmann, A., Seidl, A., Sturm, T. (eds.) Proceedings of the A3L 2005, pp. 275\u2013279. BoD, Norderstedt (2005)"}],"container-title":["Lecture Notes in Computer Science","Developments in Language Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99639-4_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,22]],"date-time":"2019-10-22T15:38:08Z","timestamp":1571758688000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99639-4_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319986531","9783319986548"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99639-4_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}