{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:17Z","timestamp":1776333497444,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642393198","type":"print"},{"value":"9783642393204","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39320-4_2","type":"book-chapter","created":{"date-parts":[[2013,7,1]],"date-time":"2013-07-01T11:22:52Z","timestamp":1372677772000},"page":"19-34","source":"Crossref","is-referenced-by-count":25,"title":["Optimising Problem Formulation for Cylindrical Algebraic Decomposition"],"prefix":"10.1007","author":[{"given":"Russell","family":"Bradford","sequence":"first","affiliation":[]},{"given":"James H.","family":"Davenport","sequence":"additional","affiliation":[]},{"given":"Matthew","family":"England","sequence":"additional","affiliation":[]},{"given":"David","family":"Wilson","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-540-85110-3_18","volume-title":"Intelligent Computer Mathematics","author":"B. Akbarpour","year":"2008","unstructured":"Akbarpour, B., Paulson, L.C.: MetiTarski: An Automatic Prover for the Elementary Functions. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) AISC\/Calculemus\/MKM 2008. LNCS (LNAI), vol.\u00a05144, pp. 217\u2013231. Springer, Heidelberg (2008)"},{"issue":"3","key":"2_CR2","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10817-009-9149-2","volume":"44","author":"B. Akbarpour","year":"2010","unstructured":"Akbarpour, B., Paulson, L.C.: MetiTarski: An automatic theorem prover for real-valued special functions. Journal of Automated Reasoning\u00a044(3), 175\u2013205 (2010)","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Bradford, R., Davenport, J.H., England, M., McCallum, S., Wilson, D.: Cylindrical algebraic decompositions for boolean combinations. In Press: Proc. ISSAC 2013 (2013), Preprint at \n                    \n                      http:\/\/opus.bath.ac.uk\/33926\/","DOI":"10.1145\/2465506.2465516"},{"issue":"4","key":"2_CR4","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/968708.968710","volume":"37","author":"C.W. Brown","year":"2003","unstructured":"Brown, C.W.: QEPCAD B: A program for computing with semi-algebraic sets using CADs. ACM SIGSAM Bulletin\u00a037(4), 97\u2013108 (2003)","journal-title":"ACM SIGSAM Bulletin"},{"key":"2_CR5","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":"2_CR6","doi-asserted-by":"crossref","unstructured":"Brown, C.W., McCallum, S.: On using bi-equational constraints in CAD construction. In: Proc. ISSAC 2005, pp. 76\u201383. ACM (2005)","DOI":"10.1145\/1073884.1073897"},{"key":"2_CR7","unstructured":"Buchberger, B., Hong, H.: Speeding up quantifier elimination by Gr\u00f6bner bases. Technical report, 91-06. RISC, Johannes Kepler University (1991)"},{"key":"2_CR8","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"},{"issue":"1:02","key":"2_CR9","first-page":"1","volume":"8","author":"C. Cohen","year":"2012","unstructured":"Cohen, C., Mahboubi, A.: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. LMCS\u00a08(1:02), 1\u201340 (2012)","journal-title":"LMCS"},{"key":"2_CR10","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":"2_CR11","doi-asserted-by":"crossref","unstructured":"Collins, G.E.: Quantifier elimination by cylindrical algebraic decomposition \u2013 20 years of progress. In: Caviness, B., Johnson, J. (eds.) 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":"2_CR12","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. Comput.\u00a012, 299\u2013328 (1991)","journal-title":"J. Symb. Comput."},{"key":"2_CR13","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 (2012)","DOI":"10.1109\/SYNASC.2012.68"},{"key":"2_CR14","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"},{"issue":"3","key":"2_CR15","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1023\/A:1006031329384","volume":"21","author":"A. Dolzmann","year":"1998","unstructured":"Dolzmann, A., Sturm, T., Weispfenning, V.: A New Approach for Automatic Theorem Proving in Real Geometry. Journal of Automated Reasoning\u00a021(3), 357\u2013380 (1998)","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR16","unstructured":"England, M.: An implementation of CAD in Maple utilising McCallum projection. Department of Computer Science Technical Report series 2013-02, University of Bath (2013), \n                    \n                      http:\/\/opus.bath.ac.uk\/33180\/"},{"key":"2_CR17","series-title":"LNAI","first-page":"136","volume-title":"CICM 2013","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)"},{"issue":"1-2","key":"2_CR18","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1016\/S0747-7171(88)80015-4","volume":"5","author":"D. Lazard","year":"1988","unstructured":"Lazard, D.: Quantifier elimination: Optimal solution for two classical examples. J. Symb. Comput.\u00a05(1-2), 261\u2013266 (1988)","journal-title":"J. Symb. Comput."},{"issue":"1-2","key":"2_CR19","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/S0747-7171(88)80010-5","volume":"5","author":"S. McCallum","year":"1988","unstructured":"McCallum, S.: An improved projection operation for cylindrical algebraic decomposition of three-dimensional space. J. Symb. Comput.\u00a05(1-2), 141\u2013161 (1988)","journal-title":"J. Symb. Comput."},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"McCallum, S.: An improved projection operation for cylindrical algebraic decomposition. In: Caviness, B., Johnson, J. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts & Monographs in Symbolic Computation, pp. 242\u2013268. Springer (1998)","DOI":"10.1007\/978-3-7091-9459-1_12"},{"key":"2_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"},{"issue":"1","key":"2_CR22","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1017\/S096012950600586X","volume":"17","author":"A. Mahboubi","year":"2007","unstructured":"Mahboubi, A.: Implementing the cylindrical algebraic decomposition within the Coq system. Math. Struct. in Comp. Science\u00a017(1), 99\u2013127 (2007)","journal-title":"Math. Struct. in Comp. Science"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/978-3-642-31374-5_24","volume-title":"Intelligent Computer Mathematics","author":"G.O. Passmore","year":"2012","unstructured":"Passmore, G.O., Paulson, L.C., de Moura, L.: Real Algebraic Strategies for MetiTarski Proofs. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS, vol.\u00a07362, pp. 358\u2013370. Springer, Heidelberg (2012)"},{"key":"2_CR24","unstructured":"Phisanbut, N.: Practical Simplification of Elementary Functions using Cylindrical Algebraic Decomposition. PhD thesis, University of Bath (2011)"},{"key":"2_CR25","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":"3","key":"2_CR26","first-page":"67","volume":"46","author":"D.J. Wilson","year":"2012","unstructured":"Wilson, D.J., Bradford, R.J., Davenport, J.H.: A repository for CAD examples. ACM Communications in Computer Algebra\u00a046(3), 67\u201369 (2012)","journal-title":"ACM Communications in Computer Algebra"},{"key":"2_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-642-31374-5_19","volume-title":"Intelligent Computer Mathematics","author":"D.J. Wilson","year":"2012","unstructured":"Wilson, D.J., Bradford, R.J., Davenport, J.H.: Speeding up cylindrical algebraic decomposition by Gr\u00f6bner bases. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS, vol.\u00a07362, pp. 280\u2013294. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39320-4_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T08:27:23Z","timestamp":1557908843000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39320-4_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642393198","9783642393204"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39320-4_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}