{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T18:04:39Z","timestamp":1746295479824},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319724522"},{"type":"electronic","value":"9783319724539"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-72453-9_22","type":"book-chapter","created":{"date-parts":[[2017,12,20]],"date-time":"2017-12-20T09:35:54Z","timestamp":1513762554000},"page":"280-285","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["The Potential and Challenges of CAD with Equational Constraints for SC-Square"],"prefix":"10.1007","author":[{"given":"James H.","family":"Davenport","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthew","family":"England","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,12,21]]},"reference":[{"key":"22_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., et al.: SC $${^2}$$ 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":"22_CR2","doi-asserted-by":"crossref","unstructured":"Bradford, R.J., Davenport, J.H., England, M., McCallum, S., Wilson, D.J.: Cylindrical algebraic decompositions for boolean combinations. In: Proceedings of ISSAC 2013, pp. 125\u2013132 (2013). https:\/\/doi.org\/10.1145\/2465506.2465516","DOI":"10.1145\/2465506.2465516"},{"key":"22_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jsc.2015.11.002","volume":"76","author":"RJ Bradford","year":"2016","unstructured":"Bradford, R.J., Davenport, J.H., England, M., McCallum, S., Wilson, D.J.: Truth table invariant cylindrical algebraic decomposition. J. Symb. Comput. 76, 1\u201335 (2016). https:\/\/doi.org\/10.1016\/j.jsc.2015.11.002","journal-title":"J. Symb. Comput."},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Proceedings of 2nd GI Conference Automata Theory & Formal Languages, pp. 134\u2013183 (1975). https:\/\/doi.org\/10.1007\/3-540-07407-4_17","DOI":"10.1007\/3-540-07407-4_17"},{"key":"22_CR5","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/978-3-7091-9459-1_2","volume-title":"Quantifier Elimination and Cylindrical Algebraic Decomposition","author":"GE Collins","year":"1998","unstructured":"Collins, G.E.: Quantifier elimination by cylindrical algebraic decomposition \u2014 twenty years of progess. In: Caviness, B.F., Johnson, J.R. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition. TEXTSMONOGR, pp. 8\u201323. Springer, Wien (1998). https:\/\/doi.org\/10.1007\/978-3-7091-9459-1_2"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-319-42432-3_20","volume-title":"Mathematical Software \u2013 ICMS 2016","author":"JH Davenport","year":"2016","unstructured":"Davenport, J.H., England, M.: Need polynomial systems be doubly-exponential? In: Greuel, G.-M., Koch, T., Paule, P., Sommese, A. (eds.) ICMS 2016. LNCS, vol. 9725, pp. 157\u2013164. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-42432-3_20"},{"issue":"1\u20132","key":"22_CR7","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S0747-7171(88)80004-X","volume":"5","author":"JH Davenport","year":"1988","unstructured":"Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5(1\u20132), 29\u201335 (1988). https:\/\/doi.org\/10.1016\/S0747-7171(88)80004-X","journal-title":"J. Symb. Comput."},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"England, M., Bradford, R., Davenport, J.H.: Improving the use of equational constraints in cylindrical algebraic decomposition. In: Proceedings of ISSAC 2015, pp. 165\u2013172. ACM (2015). https:\/\/doi.org\/10.1145\/2755996.2756678","DOI":"10.1145\/2755996.2756678"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-319-45641-6_12","volume-title":"Computer Algebra in Scientific Computing","author":"M England","year":"2016","unstructured":"England, M., Davenport, J.H.: The complexity of cylindrical algebraic decomposition with respect to polynomial degree. In: Gerdt, V.P., Koepf, W., Seiler, W.M., Vorozhtsov, E.V. (eds.) CASC 2016. LNCS, vol. 9890, pp. 172\u2013192. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-45641-6_12"},{"key":"22_CR10","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"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Lazard, D.: An improved projection operator for cylindrical algebraic decomposition. In: Proceedings of Algebraic Geometry and its Applications (1994). https:\/\/doi.org\/10.1007\/978-1-4612-2628-4_29","DOI":"10.1007\/978-1-4612-2628-4_29"},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"McCallum, S.: An Improved Projection Operation for Cylindrical Algebraic Decomposition. Ph.D. thesis, University of Wisconsin-Madison Computer Science (1984)","DOI":"10.1007\/3-540-15984-3_277"},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"McCallum, S.: On projection in CAD-based quantifier elimination with equational constraints. In: Proceedings of ISSAC 1999, pp. 145\u2013149 (1999). https:\/\/doi.org\/10.1145\/309831.309892","DOI":"10.1145\/309831.309892"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"McCallum, S.: On propagation of equational constraints in CAD-based quantifier elimination. In: Proceedings of ISSAC 2001, pp. 223\u2013231. ACM (2001). https:\/\/doi.org\/10.1145\/384101.384132","DOI":"10.1145\/384101.384132"},{"key":"22_CR15","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/j.jsc.2015.02.001","volume":"72","author":"S McCallum","year":"2016","unstructured":"McCallum, S., Hong, H.: On using Lazard\u2019s projection in CAD construction. J. Symb. Comput. 72, 65\u201381 (2016). https:\/\/doi.org\/10.1016\/j.jsc.2015.02.001","journal-title":"J. Symb. Comput."},{"key":"22_CR16","unstructured":"McCallum, S., Parusinski, A., Paunescu, L.: Arxiv (2017). https:\/\/arxiv.org\/abs\/1607.00264v2"},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A decision method for elementary algebra and geometry. University of California Press (1951). In: Caviness, B.F., Johnson, J.R. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition. TEXTSMONOGR, pp. 24\u201384. Springer, Vienna (1998) (Republished). https:\/\/doi.org\/10.1007\/978-3-7091-9459-1_3","DOI":"10.1007\/978-3-7091-9459-1_3"}],"container-title":["Lecture Notes in Computer Science","Mathematical Aspects of Computer and Information Sciences"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-72453-9_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T08:56:51Z","timestamp":1570525011000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-72453-9_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319724522","9783319724539"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-72453-9_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}