{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T03:49:13Z","timestamp":1777434553472,"version":"3.51.4"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319964171","type":"print"},{"value":"9783319964188","type":"electronic"}],"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-96418-8_55","type":"book-chapter","created":{"date-parts":[[2018,7,13]],"date-time":"2018-07-13T10:57:13Z","timestamp":1531479433000},"page":"466-474","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Polynomial Constraints and Unsat Cores in Tarski"],"prefix":"10.1007","author":[{"given":"Fernando","family":"Vale-Enriquez","sequence":"first","affiliation":[]},{"given":"Christopher W.","family":"Brown","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,14]]},"reference":[{"key":"55_CR1","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: version 2.0. In: Gupta, A., Kroening, D. (eds.) Proceedings of the 8th International Workshop on Satisfiability Modulo Theories, Edinburgh, UK (2010)"},{"issue":"4","key":"55_CR2","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)","journal-title":"ACM SIGSAM Bull."},{"key":"55_CR3","doi-asserted-by":"crossref","unstructured":"Brown, C.W.: Fast simplifications for Tarski formulas. In: Proceedings of the 2009 International Symposium on Symbolic and Algebraic Computation, ISSAC 2009, New York, NY, USA, pp. 63\u201370. ACM (2009)","DOI":"10.1145\/1576702.1576714"},{"issue":"7","key":"55_CR4","doi-asserted-by":"publisher","first-page":"859","DOI":"10.1016\/j.jsc.2011.12.012","volume":"47","author":"CW Brown","year":"2012","unstructured":"Brown, C.W.: Fast simplifications for Tarski formulas based on monomial inequalities. J. Symb. Comput. 47(7), 859\u2013882 (2012)","journal-title":"J. Symb. Comput."},{"key":"55_CR5","doi-asserted-by":"crossref","unstructured":"Brown, C.W., Davenport, J.H.: The complexity of quantifier elimination and cylindrical algebraic decomposition. In: Proceedings of the 2007 International Symposium on Symbolic and Algebraic Computation, ISSAC 2007, New York, NY, USA, pp. 54\u201360. ACM (2007)","DOI":"10.1145\/1277548.1277557"},{"key":"55_CR6","doi-asserted-by":"crossref","unstructured":"Brown, C.W., Strzebo\u0144ski, A.: Black-box\/white-box simplification and applications to quantifier elimination. In: Proceedings of the 2010 International Symposium on Symbolic and Algebraic Computation, ISSAC 2010, New York, NY, USA, pp. 69\u201376. ACM (2010)","DOI":"10.1145\/1837934.1837953"},{"key":"55_CR7","series-title":"Texts and Monographs in Symbolic Computation","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-9459-1","volume-title":"Quantifier Elimination and Cylindrical Algebraic Decomposition","year":"1998","unstructured":"Caviness, B.F., Johnson, J.R. (eds.): Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/978-3-7091-9459-1"},{"key":"55_CR8","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1145\/2110170.2110174","volume":"45","author":"C Chen","year":"2011","unstructured":"Chen, C., Davenport, J.H., Lemaire, F., Maza, M.M., Xia, B., Xiao, R., Xie, Y.: Computing the real solutions of polynomial systems with the RegularChains library in Maple. ACM Commun. Comput. Algebra 45, 166\u2013168 (2011)","journal-title":"ACM Commun. Comput. Algebra"},{"key":"55_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/978-3-642-31612-8_35","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"F Corzilius","year":"2012","unstructured":"Corzilius, F., Loup, U., Junges, S., \u00c1brah\u00e1m, E.: SMT-RAT: an SMT-compliant nonlinear real arithmetic toolbox. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 442\u2013448. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_35"},{"key":"55_CR10","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S0747-7171(88)80004-X","volume":"5","author":"JH Davenport","year":"1997","unstructured":"Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5, 29\u201335 (1997)","journal-title":"J. Symb. Comput."},{"key":"55_CR11","doi-asserted-by":"crossref","unstructured":"Dolzmann, A., Seidl, A., Sturm, T.: Efficient projection orders for CAD. In: Gutierrez, J. (ed.) Proceedings of the 2004 International Symposium on Symbolic and Algebraic Computation (ISSAC 2004), Santander, Spain, July 2004. ACM (2004)","DOI":"10.1145\/1005285.1005303"},{"key":"55_CR12","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":"55_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-319-08434-3_5","volume-title":"Intelligent Computer Mathematics","author":"M England","year":"2014","unstructured":"England, M., et al.: Problem formulation for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 45\u201360. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08434-3_5"},{"key":"55_CR14","doi-asserted-by":"crossref","unstructured":"Huang, Z., England, M., Davenport, J.M., Paulson, L.C.: Using machine learning to decide when to precondition cylindrical algebraic decomposition with Groebner bases. In: 2016 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), pp. 45\u201352, September 2016","DOI":"10.1109\/SYNASC.2016.020"},{"key":"55_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-642-31365-3_27","volume-title":"Automated Reasoning","author":"D Jovanovi\u0107","year":"2012","unstructured":"Jovanovi\u0107, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 339\u2013354. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_27"},{"issue":"5","key":"55_CR16","doi-asserted-by":"publisher","first-page":"432","DOI":"10.1093\/comjnl\/36.5.432","volume":"36","author":"S McCallum","year":"1993","unstructured":"McCallum, S.: Solving polynomial strict inequalities using cylindrical algebraic decomposition. Comput. J. 36(5), 432\u2013438 (1993)","journal-title":"Comput. J."},{"key":"55_CR17","doi-asserted-by":"publisher","first-page":"2006","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-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53, 2006 (2006)","journal-title":"J. ACM"},{"key":"55_CR18","unstructured":"Papachristodoulou, A., Anderson, J., Valmorbida, G., Prajna, S., Seiler, P., Parrilo, P.A.: SOSTOOLS: sum of squares optimization toolbox for MATLAB (2013). http:\/\/www.eng.ox.ac.uk\/control\/sostools . http:\/\/arxiv.org\/abs\/1310.4716"},{"key":"55_CR19","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1006\/jsco.1999.0327","volume":"29","author":"A Strzebonski","year":"2000","unstructured":"Strzebonski, A.: Solving systems of strict polynomial inequalities. J. Symb. Comput. 29, 471\u2013480 (2000)","journal-title":"J. Symb. Comput."},{"key":"55_CR20","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry, Second edn. University of California Press, Berkeley (1951). rev. Reprinted in [7]","DOI":"10.1525\/9780520348097"},{"issue":"1\u20132","key":"55_CR21","doi-asserted-by":"publisher","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. J. Symb. Comput. 5(1\u20132), 3\u201327 (1988)","journal-title":"J. Symb. Comput."}],"container-title":["Lecture Notes in Computer Science","Mathematical Software \u2013 ICMS 2018"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-96418-8_55","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,27]],"date-time":"2022-08-27T14:00:25Z","timestamp":1661608825000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-96418-8_55"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319964171","9783319964188"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-96418-8_55","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}