{"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":1776333497505,"version":"3.51.2"},"publisher-location":"Cham","reference-count":50,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319084336","type":"print"},{"value":"9783319084343","type":"electronic"}],"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_8","type":"book-chapter","created":{"date-parts":[[2014,6,30]],"date-time":"2014-06-30T23:14:35Z","timestamp":1404170075000},"page":"92-107","source":"Crossref","is-referenced-by-count":29,"title":["Applying Machine Learning to the Problem of Choosing a Heuristic to Select the Variable Ordering for Cylindrical Algebraic Decomposition"],"prefix":"10.1007","author":[{"given":"Zongyan","family":"Huang","sequence":"first","affiliation":[]},{"given":"Matthew","family":"England","sequence":"additional","affiliation":[]},{"given":"David","family":"Wilson","sequence":"additional","affiliation":[]},{"given":"James H.","family":"Davenport","sequence":"additional","affiliation":[]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[]},{"given":"James","family":"Bridge","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"8_CR1","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.: 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":"8_CR2","unstructured":"Alpaydin, E.: Introduction to machine learning. MIT Press (2004)"},{"key":"8_CR3","doi-asserted-by":"publisher","first-page":"865","DOI":"10.1137\/0213054","volume":"13","author":"D. Arnon","year":"1984","unstructured":"Arnon, D., Collins, G., McCallum, S.: Cylindrical algebraic decomposition I: The basic algorithm. SIAM Journal of Computing\u00a013, 865\u2013877 (1984)","journal-title":"SIAM Journal of Computing"},{"issue":"5","key":"8_CR4","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1093\/bioinformatics\/16.5.412","volume":"16","author":"P. Baldi","year":"2000","unstructured":"Baldi, P., Brunak, S., Chauvin, Y., Andersen, C.A., Nielsen, H.: Assessing the accuracy of prediction algorithms for classification: an overview. Bioinformatics\u00a016(5), 412\u2013424 (2000)","journal-title":"Bioinformatics"},{"key":"8_CR5","unstructured":"Basu, S.: Algorithms in real algebraic geometry: A survey (2011), www.math.purdue.edu\/~sbasu\/raag_survey2011_final.pdf"},{"key":"8_CR6","unstructured":"Boyan, J., Freitag, D., Joachims, T.: A machine learning architecture for optimizing web search engines. In: AAAI Workshop on Internet Based Information Systems, pp. 1\u20138 (1996)"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Bradford, R., Davenport, J., 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":"8_CR8","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":"8_CR9","unstructured":"Bridge, J.P.: Machine learning and automated theorem proving. University of Cambridge Computer Laboratory Technical Report UCAM-CL-TR-792 (2010), http:\/\/www.cl.cam.ac.uk\/techreports\/UCAM-CL-TR-792.pdf"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Bridge, J., Holden, S., Paulson, L.: Machine learning for first-order theorem proving. Journal of Automated Reasoning, 1\u201332 (2014)","DOI":"10.1007\/s10817-014-9301-5"},{"issue":"5","key":"8_CR11","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1006\/jsco.2001.0463","volume":"32","author":"C. Brown","year":"2001","unstructured":"Brown, C.: Improved projection for cylindrical algebraic decomposition. Journal of Symbolic Computation\u00a032(5), 447\u2013465 (2001)","journal-title":"Journal of Symbolic Computation"},{"issue":"4","key":"8_CR12","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/968708.968710","volume":"37","author":"C. Brown","year":"2003","unstructured":"Brown, C.: 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":"8_CR13","unstructured":"Brown, C.: Companion to the Tutorial: Cylindrical algebraic decomposition. Presented at ISSAC 2004 (2004), www.usna.edu\/Users\/cs\/wcbrown\/research\/ISSAC04\/handout.pdf"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Brown, C., Davenport, J.: The complexity of quantifier elimination and cylindrical algebraic decomposition. In: Proc. ISSAC 2007, pp. 54\u201360. ACM (2007)","DOI":"10.1145\/1277548.1277557"},{"key":"8_CR15","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.1016\/j.jsc.2005.09.011","volume":"41","author":"C. Brown","year":"2006","unstructured":"Brown, C., Kahoui, M.E., Novotni, D., Weber, A.: Algorithmic methods for investigating equilibria in epidemic modelling. Journal of Symbolic Computation\u00a041, 1157\u20131173 (2006)","journal-title":"Journal of Symbolic Computation"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Carette, J.: Understanding expression simplification. In: Proc. ISSAC 2004, pp. 72\u201379. ACM (2004)","DOI":"10.1145\/1005285.1005298"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Chen, C., Maza, M.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":"8_CR18","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":"8_CR19","doi-asserted-by":"crossref","unstructured":"Collins, G.: 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":"8_CR20","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1016\/S0747-7171(08)80152-6","volume":"12","author":"G. Collins","year":"1991","unstructured":"Collins, G., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. Journal of Symbolic Computation\u00a012, 299\u2013328 (1991)","journal-title":"Journal of Symbolic Computation"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Cristianini, N., Shawe-Taylor, J.: An introduction to support vector machines and other kernel-based learning methods. Cambridge University Press (2000)","DOI":"10.1017\/CBO9780511801389"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Davenport, J., 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":"8_CR23","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":"2","key":"8_CR24","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/261320.261324","volume":"31","author":"A. Dolzmann","year":"1997","unstructured":"Dolzmann, A., Sturm, T.: REDLOG: Computer algebra meets computer logic. SIGSAM Bulletin\u00a031(2), 2\u20139 (1997)","journal-title":"SIGSAM Bulletin"},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"Dolzmann, A., Sturm, T., Weispfenning, V.: Real quantifier elimination in practice. In: Algorithmic Algebra and Number Theory, pp. 221\u2013247. Springer (1998)","DOI":"10.1007\/978-3-642-59932-3_11"},{"key":"8_CR26","unstructured":"England, M.: An implementation of CAD in Maple utilising problem formulation, equational constraints and truth-table invariance. University of Bath Department of Computer Science Technical Report 2013-04 (2013), http:\/\/opus.bath.ac.uk\/35636\/"},{"key":"8_CR27","unstructured":"Forsyth, R., Rada, R.: Machine learning: Applications in expert systems and information retrieval. Halsted Press (1986)"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Fotiou, I., Parrilo, P., Morari, M.: Nonlinear parametric optimization using cylindrical algebraic decomposition. In: 2005 European Control Conference on Decision and Control, CDC-ECC 2005, pp. 3735\u20133740 (2005)","DOI":"10.1109\/CDC.2005.1582743"},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"Hong, H.: An improvement of the projection operator in cylindrical algebraic decomposition. In: Proc. ISSAC 1990, pp. 261\u2013264. ACM (1990)","DOI":"10.1145\/96877.96943"},{"issue":"5","key":"8_CR30","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1016\/0893-6080(89)90020-8","volume":"2","author":"K. Hornik","year":"1989","unstructured":"Hornik, K., Stinchcombe, M., White, H.: Multilayer feedforward networks are universal approximators. Neural Networks\u00a02(5), 359\u2013366 (1989)","journal-title":"Neural Networks"},{"key":"8_CR31","unstructured":"Huang, Z., Paulson, L.: An application of machine learning to rcf decision procedures. In: Proc. 20th Automated Reasoning Workshop (2013)"},{"key":"8_CR32","unstructured":"Hsu, C., Chang, C., Lin, C.: A practical guide to support vector classification (2003)"},{"key":"8_CR33","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"},{"key":"8_CR34","unstructured":"Joachims, T.: Making large-scale SVM learning practical. In: Advances in Kernel Methods - Support Vector Learning, pp. 169\u2013184. MIT Press (1999)"},{"key":"8_CR35","doi-asserted-by":"crossref","unstructured":"Joachims, T.: A support vector method for multivariate performance measures. In: Proc. 22nd Intl. Conf. on Machine Learning, pp. 377\u2013384. ACM (2005)","DOI":"10.1145\/1102351.1102399"},{"key":"8_CR36","series-title":"Lecture Notes in Computer Science","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, vol.\u00a07364, pp. 339\u2013354. Springer, Heidelberg (2012)"},{"key":"8_CR37","doi-asserted-by":"crossref","unstructured":"McCallum, S.: An improved projection operation for cylindrical algebraic decomposition. In: 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":"8_CR38","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":"4","key":"8_CR39","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/BF02478259","volume":"5","author":"W.S. McCulloch","year":"1943","unstructured":"McCulloch, W.S., Pitts, W.: A logical calculus of the ideas immanent in nervous activity. The Bulletin of Mathematical Biophysics\u00a05(4), 115\u2013133 (1943)","journal-title":"The Bulletin of Mathematical Biophysics"},{"issue":"6","key":"8_CR40","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1037\/h0042519","volume":"65","author":"F. Rosenblatt","year":"1958","unstructured":"Rosenblatt, F.: The perceptron: a probabilistic model for information storage and organization in the brain. Psychological Review\u00a065(6), 386 (1958)","journal-title":"Psychological Review"},{"key":"8_CR41","doi-asserted-by":"crossref","unstructured":"Sch\u00f6lkopf, B., Tsuda, K., Vert, J.-P.: Kernel methods in computational biology. MIT Press (2004)","DOI":"10.7551\/mitpress\/4057.001.0001"},{"issue":"1","key":"8_CR42","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/505282.505283","volume":"34","author":"F. Sebastiani","year":"2002","unstructured":"Sebastiani, F.: Machine learning in automated text categorization. ACM Computing Surveys (CSUR)\u00a034(1), 1\u201347 (2002)","journal-title":"ACM Computing Surveys (CSUR)"},{"key":"8_CR43","doi-asserted-by":"crossref","unstructured":"Shawe-Taylor, J., Cristianini, N.: Kernel methods for pattern analysis. Cambridge University Press (2004)","DOI":"10.1017\/CBO9780511809682"},{"issue":"3","key":"8_CR44","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1023\/A:1008942012299","volume":"8","author":"P. Stone","year":"2000","unstructured":"Stone, P., Veloso, M.: Multiagent systems: A survey from a machine learning perspective. Autonomous Robots\u00a08(3), 345\u2013383 (2000)","journal-title":"Autonomous Robots"},{"issue":"9","key":"8_CR45","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. Journal of Symbolic Computation\u00a041(9), 1021\u20131038 (2006)","journal-title":"Journal of Symbolic Computation"},{"key":"8_CR46","doi-asserted-by":"crossref","unstructured":"Strzebo\u0144ski, A.: Solving polynomial systems over semialgebraic sets represented by cylindrical algebraic formulas. In: Proc. ISSAC 2012, pp. 335\u2013342. ACM (2012)","DOI":"10.1145\/2442829.2442877"},{"key":"8_CR47","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A decision method for elementary algebra and geometry. In: Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation, pp. 24\u201384. Springer (1998)","DOI":"10.1007\/978-3-7091-9459-1_3"},{"issue":"3","key":"8_CR48","first-page":"67","volume":"46","author":"D. Wilson","year":"2012","unstructured":"Wilson, D., Bradford, R., Davenport, J.: A repository for CAD examples. ACM Communications in Computer Algebra\u00a046(3), 67\u201369 (2012)","journal-title":"ACM Communications in Computer Algebra"},{"key":"8_CR49","unstructured":"Wilson, D., Davenport, J., England, M., Bradford, R.: A \u201cpiano movers\u201d problem reformulated. In: Proc. SYNASC 2013. IEEE (2013)"},{"key":"8_CR50","unstructured":"The benchmarks used in solving nonlinear arithmetic. New York University (2012), http:\/\/cs.nyu.edu\/~dejan\/nonlinear\/"}],"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_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,12]],"date-time":"2019-08-12T01:50:24Z","timestamp":1565574624000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08434-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319084336","9783319084343"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08434-3_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}