{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:59:48Z","timestamp":1762459188635},"reference-count":45,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2014,6,1]],"date-time":"2014-06-01T00:00:00Z","timestamp":1401580800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Math.Comput.Sci."],"published-print":{"date-parts":[[2014,6]]},"DOI":"10.1007\/s11786-014-0191-z","type":"journal-article","created":{"date-parts":[[2014,6,12]],"date-time":"2014-06-12T03:09:10Z","timestamp":1402542550000},"page":"263-288","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Cylindrical Algebraic Sub-Decompositions"],"prefix":"10.1007","volume":"8","author":[{"given":"D. J.","family":"Wilson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R. J.","family":"Bradford","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J. H.","family":"Davenport","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"England","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,6,13]]},"reference":[{"key":"191_CR1","doi-asserted-by":"crossref","first-page":"865","DOI":"10.1137\/0213054","volume":"13","author":"D. Arnon","year":"1984","unstructured":"Arnon D., Collins G.E., McCallum S.: Cylindrical algebraic decomposition I: the basic algorithm. SIAM J. Comput. 13, 865\u2013877 (1984)","journal-title":"SIAM J. Comput."},{"key":"191_CR2","unstructured":"Backelin, J.: Square multiples n give infinitely many cyclic n-roots. Matematiska Institutionen Reports Series. Stockholms Universitet (1989)"},{"key":"191_CR3","doi-asserted-by":"crossref","unstructured":"Bradford, R., Davenport, J.H.: Towards better simplification of elementary functions. In: Proceedings of the ISSAC\u201902, pp. 16\u201322. ACM (2002)","DOI":"10.1145\/780506.780509"},{"key":"191_CR4","doi-asserted-by":"crossref","unstructured":"Bradford, R., Davenport, J.H., England, M. McCallum, S., Wilson, D.: Cylindrical algebraic decompositions for boolean combinations. In: Proceedings of the ISSAC\u201913, pp. 125\u2013132. ACM (2013)","DOI":"10.1145\/2465506.2465516"},{"key":"191_CR5","unstructured":"Bradford, R., Davenport, J.H., England, M., McCallum, S., Wilson, D.: Truth table invariant cylindrical algebraic decomposition. http:\/\/opus.bath.ac.uk\/38146\/ (2014 submitted, preprint)"},{"key":"191_CR6","doi-asserted-by":"crossref","unstructured":"Bradford, R., Davenport, J.H., England, M., Wilson, D.: Optimising problem formulations for cylindrical algebraic decomposition. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. Intelligent Computer Mathematics. LNCS, vol. 7961, pp. 19\u201334. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-39320-4_2"},{"issue":"5","key":"191_CR7","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1006\/jsco.2001.0463","volume":"32","author":"C.W. Brown","year":"2001","unstructured":"Brown C.W.: Improved projection for cylindrical algebraic decomposition. J. Symb. Comput. 32(5), 447\u2013465 (2001)","journal-title":"J. Symb. Comput."},{"issue":"4","key":"191_CR8","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1145\/968708.968710","volume":"37","author":"C.W. Brown","year":"2003","unstructured":"Brown C.W.: An overview of 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":"191_CR9","doi-asserted-by":"crossref","unstructured":"Brown, C.W.: The McCallum projection, lifting, and order-invariance. Technical report, US Naval Academy, Computer Science Department (2005)","DOI":"10.21236\/ADA460719"},{"key":"191_CR10","doi-asserted-by":"crossref","unstructured":"Brown, C.W.: Constructing a single open cell in a cylindrical algebraic decomposition. In: Proceedings of the ISSAC\u201913, pp. 133\u2013140. ACM (2013)","DOI":"10.1145\/2465506.2465952"},{"key":"191_CR11","doi-asserted-by":"crossref","unstructured":"Brown, C.W., Davenport, J.H.: The complexity of quantifier elimination and cylindrical algebraic decomposition. In: Proceedings of the ISSAC\u201907, pp. 54\u201360. ACM (2007)","DOI":"10.1145\/1277548.1277557"},{"key":"191_CR12","doi-asserted-by":"crossref","first-page":"1157","DOI":"10.1016\/j.jsc.2005.09.011","volume":"41","author":"C.W. Brown","year":"2006","unstructured":"Brown C.W., El Kahoui M., Novotni D., Weber A.: Algorithmic methods for investigating equilibria in epidemic modelling. J. Symb. Comput. 41, 1157\u20131173 (2006)","journal-title":"J. Symb. Comput."},{"key":"191_CR13","doi-asserted-by":"crossref","unstructured":"Brown, C.W., McCallum, S.: On using bi-equational constraints in CAD construction. In: Proceedings of the ISSAC\u201905, pp. 76\u201383. ACM (2005)","DOI":"10.1145\/1073884.1073897"},{"key":"191_CR14","unstructured":"Burr, M.A.: Applications of continuous amortization to bisection-based root isolation. http:\/\/arxiv.org\/abs\/1309.5991 (2013, preprint)"},{"key":"191_CR15","unstructured":"Chen, C., Moreno Maza, M.: An incremental algorithm for computing cylindrical algebraic decompositions. In: Proceedings of the ASCM\u201912. Springer, Berlin (2012, preprint). arXiv:1210.5543"},{"key":"191_CR16","doi-asserted-by":"crossref","unstructured":"Chen, C., Moreno Maza, M., Xia, B., Yang, L.: Computing cylindrical algebraic decomposition via triangular decomposition. In: Proceedings of the ISSAC\u201909, pp. 95\u2013102. ACM (2009)","DOI":"10.1145\/1576702.1576718"},{"key":"191_CR17","doi-asserted-by":"crossref","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages, pp. 134\u2013183. Springer. Berlin (1975)","DOI":"10.1007\/3-540-07407-4_17"},{"key":"191_CR18","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., Hong H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput. 12, 299\u2013328 (1991)","journal-title":"J. Symb. Comput."},{"key":"191_CR19","unstructured":"Davenport, J.H.: Computer algebra for cylindrical algebraic decomposition. Technical Report TRITA-NA-8511, NADA KTH Stockholm. Reissued as Bath Computer Science Technical report 88-10. http:\/\/staff.bath.ac.uk\/masjhd\/TRITA.pdf (1985)"},{"issue":"1\u20132","key":"191_CR20","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1145\/12917.12919","volume":"20","author":"J.H. Davenport","year":"1986","unstructured":"Davenport J.H.: A \u201cPiano-Movers\u201d problem. SIGSAM Bull. 20(1\u20132), 15\u201317 (1986)","journal-title":"SIGSAM Bull."},{"key":"191_CR21","doi-asserted-by":"crossref","unstructured":"Davenport, J.H., Bradford, R., England, M., Wilson, D.: Program verification in the presence of complex numbers, functions with branch cuts etc. In: Proceedings of the SYNASC\u201912, pp. 83\u201388. IEEE (2012)","DOI":"10.1109\/SYNASC.2012.68"},{"issue":"1\u20132","key":"191_CR22","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1016\/S0747-7171(88)80004-X","volume":"5","author":"J.H. Davenport","year":"1988","unstructured":"Davenport J.H., Heintz J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5(1\u20132), 29\u201335 (1988)","journal-title":"J. Symb. Comput."},{"key":"191_CR23","doi-asserted-by":"crossref","unstructured":"Dolzmann, A., Seidl, A., Sturm, T.: Efficient projection orders for CAD. In: Proceedings of the ISSAC\u201904, pp. 111\u2013118. ACM (2004)","DOI":"10.1145\/1005285.1005303"},{"key":"191_CR24","unstructured":"England, M.: An implementation of CAD in Maple utilising McCallum projection. Department of Computer Science Technical Report series 2013-02, University of Bath. http:\/\/opus.bath.ac.uk\/33180\/ (2013)"},{"key":"191_CR25","unstructured":"England, M.: An implementation of CAD in Maple utilising problem formulation, equational constraints and truth-table invariance. Department of Computer Science Technical Report series 2013-04, University of Bath. http:\/\/opus.bath.ac.uk\/35636\/ (2013)"},{"key":"191_CR26","first-page":"136","volume-title":"Intelligent Computer Mathematics. LNCS, vol. 7961","author":"M. England","year":"2013","unstructured":"England M., Bradford R., Davenport J.H., Wilson D.: Understanding branch cuts of expressions. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) Intelligent Computer Mathematics. LNCS, vol. 7961, pp. 136\u2013151. Springer, Berlin (2013)"},{"key":"191_CR27","unstructured":"Fotiou, I.A., Parrilo, P.A., Morari, M.: Nonlinear parametric optimization using cylindrical algebraic decomposition. In: Decision and Control, 2005 and 2005 European Control Conference. CDC-ECC \u201905, pp. 3735\u20133740 (2005)"},{"key":"191_CR28","doi-asserted-by":"crossref","unstructured":"Hong, H.: An improvement of the projection operator in cylindrical algebraic decomposition. In: Proceedings of the ISSAC\u201990, pp. 261\u2013264. ACM (1990)","DOI":"10.1145\/96877.96943"},{"key":"191_CR29","doi-asserted-by":"crossref","unstructured":"Iwane, H., Yanami, H., Anai, H., Yokoyama, K.: An effective implementation of a symbolic-numeric cylindrical algebraic decomposition for quantifier elimination. In: Proceedings of the SNC\u201909, pp. 55\u201364 (2009)","DOI":"10.1145\/1577190.1577203"},{"key":"191_CR30","unstructured":"Malladi, H.K., Dukkipati, A.: A preprocessor based on clause normal forms and virtual substitutions to parallelize cylindrical algebraic decomposition. http:\/\/arxiv.org\/abs\/1112.5352v3 (2013, preprint)"},{"issue":"5","key":"191_CR31","doi-asserted-by":"crossref","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":"191_CR32","unstructured":"McCallum, S.: A computer algebra approach to path finding in the plane. In: Harland J. (ed.) Proceedings of Computing: The Australasian Theory Symposium (CATS), pp. 44\u201350 (1997)"},{"key":"191_CR33","doi-asserted-by":"crossref","unstructured":"McCallum, S.: An improved projection operation for cylindrical algebraic decomposition. In: Caviness, B., Johnson, J. Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation, pp. 242\u2013268. Springer, Berlin (1998)","DOI":"10.1007\/978-3-7091-9459-1_12"},{"key":"191_CR34","doi-asserted-by":"crossref","unstructured":"McCallum, S.: On projection in CAD-based quantifier elimination with equational constraint. In: Proceedings of the ISSAC\u201999, pp. 145\u2013149. ACM (1999)","DOI":"10.1145\/309831.309892"},{"key":"191_CR35","doi-asserted-by":"crossref","unstructured":"McCallum, S.: On propagation of equational constraints in CAD-based quantifier elimination. In: Proceedings of the ISSAC\u201901, pp. 223\u2013231. ACM (2001)","DOI":"10.1145\/384101.384132"},{"key":"191_CR36","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-642-32347-8_1","volume-title":"Interactive Theorem Proving. LNCS, vol. 7406","author":"L.C. Paulson","year":"2012","unstructured":"Paulson L.C.: Metitarski: past and future. In: Beringer, L., Felty, A. (eds.) Interactive Theorem Proving. LNCS, vol. 7406, pp. 1\u201310. Springer, Berlin (2012)"},{"issue":"3","key":"191_CR37","first-page":"132","volume":"44","author":"N. Phisanbut","year":"2010","unstructured":"Phisanbut N., Bradford R.J., Davenport J.H.: Geometry of branch cuts. ACM Commun. Comput. Algebra 44(3), 132\u2013135 (2010)","journal-title":"ACM Commun. Comput. Algebra"},{"key":"191_CR38","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1016\/0196-8858(83)90014-3","volume":"4","author":"J.T. Schwartz","year":"1983","unstructured":"Schwartz J.T., Sharir M.: On the \u201cPiano-Movers\u201d problem: II. General techniques for computing topological properties of real algebraic manifolds. Adv. Appl. Math. 4, 298\u2013351 (1983)","journal-title":"Adv. Appl. Math."},{"key":"191_CR39","doi-asserted-by":"crossref","unstructured":"Seidl, A., Sturm, T.: A generic projection operator for partial cylindrical algebraic decomposition. In: Proceedings of the ISSAC\u201903, pp. 240\u2013247. ACM (2003)","DOI":"10.1145\/860854.860903"},{"issue":"3","key":"191_CR40","doi-asserted-by":"crossref","first-page":"471","DOI":"10.1006\/jsco.1999.0327","volume":"29","author":"A. Strzebo\u0144ski","year":"2000","unstructured":"Strzebo\u0144ski A.: Solving systems of strict polynomial inequalities. J. Symb. Comput. 29(3), 471\u2013480 (2000)","journal-title":"J. Symb. Comput."},{"issue":"9","key":"191_CR41","doi-asserted-by":"crossref","first-page":"1021","DOI":"10.1016\/j.jsc.2006.06.004","volume":"41","author":"A. Strzebo\u0144ski","year":"2006","unstructured":"Strzebo\u0144ski A.: Cylindrical algebraic decomposition using validated numerics. J. Symb. Comput. 41(9), 1021\u20131038 (2006)","journal-title":"J. Symb. Comput."},{"key":"191_CR42","doi-asserted-by":"crossref","unstructured":"Strzebo\u0144ski, A.: Computation with semialgebraic sets represented by cylindrical algebraic formulas. In: Proceedings of the ISSAC\u201910, pp. 61\u201368. ACM (2010)","DOI":"10.1145\/1837934.1837952"},{"key":"191_CR43","doi-asserted-by":"crossref","unstructured":"Strzebo\u0144ski, A.: Solving polynomial systems over semialgebraic sets represented by cylindrical algebraic formulas. In: Proceedings of the ISSAC\u201912, pp. 335\u2013342. ACM (2012)","DOI":"10.1145\/2442829.2442877"},{"key":"191_CR44","unstructured":"Wilson, D., Davenport, J.H., England, M., Bradford, R.: A \u201cPiano Movers\u201d problem reformulated. In: Proceedings of the SYNASC\u201913. IEEE (2013)"},{"key":"191_CR45","unstructured":"Wilson, D., England, M.: Layered cylindrical algebraic decomposition. Department of Computer Science Technical Report series 2013-05, University of Bath. http:\/\/opus.bath.ac.uk\/36712\/ (2013)"}],"container-title":["Mathematics in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11786-014-0191-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11786-014-0191-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11786-014-0191-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,11]],"date-time":"2019-08-11T09:08:51Z","timestamp":1565514531000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11786-014-0191-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,6]]},"references-count":45,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,6]]}},"alternative-id":["191"],"URL":"https:\/\/doi.org\/10.1007\/s11786-014-0191-z","relation":{},"ISSN":["1661-8270","1661-8289"],"issn-type":[{"value":"1661-8270","type":"print"},{"value":"1661-8289","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,6]]}}}