{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T02:01:59Z","timestamp":1760061719450},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319084336"},{"type":"electronic","value":"9783319084343"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08434-3_5","type":"book-chapter","created":{"date-parts":[[2014,7,1]],"date-time":"2014-07-01T03:14:35Z","timestamp":1404184475000},"page":"45-60","source":"Crossref","is-referenced-by-count":12,"title":["Problem Formulation for Truth-Table Invariant Cylindrical Algebraic Decomposition by Incremental Triangular Decomposition"],"prefix":"10.1007","author":[{"given":"Matthew","family":"England","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Russell","family":"Bradford","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Changbo","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"James H.","family":"Davenport","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marc Moreno","family":"Maza","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Wilson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","doi-asserted-by":"publisher","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.\u00a013, 865\u2013877 (1984)","journal-title":"SIAM J. Comput."},{"issue":"1-2","key":"5_CR2","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1016\/S0747-7171(88)80014-2","volume":"5","author":"D.S. Arnon","year":"1988","unstructured":"Arnon, D.S., Mignotte, M.: On mechanical quantifier elimination for elementary algebra and geometry. J. Symb. Comp.\u00a05(1-2), 237\u2013259 (1988)","journal-title":"J. Symb. Comp."},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Bradford, R., Chen, C., Davenport, J.H., England, M., Moreno Maza, M., Wilson, D.: Truth table invariant cylindrical algebraic decomposition by regular chains (submitted, 2014), Preprint: http:\/\/opus.bath.ac.uk\/38344\/","DOI":"10.1007\/978-3-319-10515-4_4"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Bradford, R., Davenport, J.H., England, M., McCallum, S., Wilson, D.: Cylindrical algebraic decompositions for boolean combinations. In: Proc. ISSAC 2013, pp. 125\u2013132. ACM (2013)","DOI":"10.1145\/2465506.2465516"},{"key":"5_CR5","unstructured":"Bradford, R., Davenport, J.H., England, M., McCallum, S., Wilson, D.: Truth table invariant cylindrical algebraic decomposition (submitted, 2014), Preprint: http:\/\/opus.bath.ac.uk\/38146\/"},{"key":"5_CR6","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-642-39320-4_2","volume-title":"Intelligent Computer Mathematics","author":"R. Bradford","year":"2013","unstructured":"Bradford, R., Davenport, J.H., England, M., Wilson, D.: Optimising problem formulation for cylindrical algebraic decomposition. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol.\u00a07961, pp. 19\u201334. Springer, Heidelberg (2013)"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Brown, C.W., Davenport, J.H.: The complexity of quantifier elimination and cylindrical algebraic decomposition. In: Proc. ISSAC 2007, pp. 54\u201360. ACM (2007)","DOI":"10.1145\/1277548.1277557"},{"key":"5_CR8","doi-asserted-by":"publisher","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. Symbolic Computation\u00a041, 1157\u20131173 (2006)","journal-title":"J. Symbolic Computation"},{"key":"5_CR9","unstructured":"Chen, C., Moreno Maza, M.: An incremental algorithm for computing cylindrical algebraic decompositions. In: Proc. ASCM 2012. Springer (2012) (to appear), Preprint: arXiv:1210.5543v1"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Chen, C., Moreno Maza, M., Xia, B., Yang, L.: Computing cylindrical algebraic decomposition via triangular decomposition. In: Proc. ISSAC 2009, pp. 95\u2013102. ACM (2009)","DOI":"10.1145\/1576702.1576718"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Automata Theory and Formal Languages","author":"G.E. Collins","year":"1975","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol.\u00a033, pp. 134\u2013183. Springer, Heidelberg (1975)"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Collins, G.E.: Quantifier elimination by cylindrical algebraic decomposition \u2013 20 years of progress. In: Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts & Monographs in Symbolic Computation, pp. 8\u201323. Springer (1998)","DOI":"10.1007\/978-3-7091-9459-1_2"},{"key":"5_CR13","doi-asserted-by":"publisher","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. Comp.\u00a012, 299\u2013328 (1991)","journal-title":"J. Symb. Comp."},{"key":"5_CR14","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: Proc. SYNASC 2012, pp. 83\u201388. IEEE (2012)","DOI":"10.1109\/SYNASC.2012.68"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Dolzmann, A., Seidl, A., Sturm, T.: Efficient projection orders for CAD. In: Proc. ISSAC 2004, pp. 111\u2013118. ACM (2004)","DOI":"10.1145\/1005285.1005303"},{"key":"5_CR16","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-642-39320-4_9","volume-title":"Intelligent Computer Mathematics","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.) CICM 2013. LNCS (LNAI), vol.\u00a07961, pp. 136\u2013151. Springer, Heidelberg (2013)"},{"key":"5_CR17","unstructured":"England, M.: An implementation of CAD in Maple utilising problem formulation, equational constraints and truth-table invariance. Uni. Bath, Dept. Comp. Sci. Tech. Report Series, 2013-04 (2013), http:\/\/opus.bath.ac.uk\/35636\/"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Fotiou, I.A., Parrilo, P.A., Morari, M.: Nonlinear parametric optimization using cylindrical algebraic decomposition. In: Proc. CDC-ECC 2005, pp. 3735\u20133740 (2005)","DOI":"10.1109\/CDC.2005.1582743"},{"key":"5_CR19","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: Proc. SNC 2009, pp. 55\u201364 (2009)","DOI":"10.1145\/1577190.1577203"},{"issue":"3","key":"5_CR20","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1145\/1088309.1088312","volume":"9","author":"W. Kahan","year":"1975","unstructured":"Kahan, W.: Problem #9: an ellipse problem. SIGSAM Bull.\u00a09(3), 11\u201312 (1975)","journal-title":"SIGSAM Bull."},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"McCallum, S.: On projection in CAD-based quantifier elimination with equational constraint. In: Proc. ISSAC 1999, pp. 145\u2013149. ACM (1999)","DOI":"10.1145\/309831.309892"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-32347-8_1","volume-title":"Interactive Theorem Proving","author":"L.C. Paulson","year":"2012","unstructured":"Paulson, L.C.: MetiTarski: Past and future. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol.\u00a07406, pp. 1\u201310. Springer, Heidelberg (2012)"},{"key":"5_CR23","doi-asserted-by":"publisher","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.\u00a04, 298\u2013351 (1983)","journal-title":"Adv. Appl. Math."},{"issue":"9","key":"5_CR24","doi-asserted-by":"publisher","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. Comp.\u00a041(9), 1021\u20131038 (2006)","journal-title":"J. Symb. Comp."}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08434-3_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,12]],"date-time":"2019-08-12T05:50:00Z","timestamp":1565589000000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08434-3_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319084336","9783319084343"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08434-3_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}