{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:08:36Z","timestamp":1762459716697},"reference-count":101,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2019,4,3]],"date-time":"2019-04-03T00:00:00Z","timestamp":1554249600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/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":[[2019,12]]},"DOI":"10.1007\/s11786-019-00394-8","type":"journal-article","created":{"date-parts":[[2019,4,4]],"date-time":"2019-04-04T03:53:59Z","timestamp":1554350039000},"page":"461-488","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Using Machine Learning to Improve Cylindrical Algebraic Decomposition"],"prefix":"10.1007","volume":"13","author":[{"given":"Zongyan","family":"Huang","sequence":"first","affiliation":[]},{"given":"Matthew","family":"England","sequence":"additional","affiliation":[]},{"given":"David J.","family":"Wilson","sequence":"additional","affiliation":[]},{"given":"James","family":"Bridge","sequence":"additional","affiliation":[]},{"given":"James H.","family":"Davenport","sequence":"additional","affiliation":[]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,4,3]]},"reference":[{"key":"394_CR1","doi-asserted-by":"crossref","unstructured":"\u00c1brah\u00e1m, E., Abbott, J., Becker, B., Bigatti, A.M., Brain, M., Buchberger, B., Cimatti, A., Davenport, J.H., England, M., Fontaine, P., Forrest, S., Griggio, A., Kroening, D., Seiler, W.M., Sturm, T.: $${{\\sf SC}}^2$$ SC 2 : satisfiability checking meets symbolic computation. In: Kohlhase, M., Johansson, M., Miller, B., de Moura, L., Tompa, F. (eds.) Intelligent Computer Mathematics: Proceedings CICM 2016, volume 9791 of Lecture Notes in Computer Science, pp. 28\u201343. Springer (2016)","DOI":"10.1007\/978-3-319-42547-4_3"},{"key":"394_CR2","volume-title":"Introduction to Machine Learning","author":"E Alpaydin","year":"2004","unstructured":"Alpaydin, E.: Introduction to Machine Learning. MIT Press, Cambridge (2004)"},{"key":"394_CR3","doi-asserted-by":"crossref","unstructured":"Arai, N.H., Matsuzaki, T., Iwane, H., Anai, H.: Mathematics by machine. In: Proceedings of the 39th International Symposium on Symbolic and Algebraic Computation, ISSAC \u201914, pp. 1\u20138. ACM (2014)","DOI":"10.1145\/2608628.2627488"},{"key":"394_CR4","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."},{"issue":"5","key":"394_CR5","doi-asserted-by":"crossref","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.F., Nielsen, H.: Assessing the accuracy of prediction algorithms for classification: an overview. Bioinformatics 16(5), 412\u2013424 (2000)","journal-title":"Bioinformatics"},{"key":"394_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-33099-2","volume-title":"Algorithms in Real Algebraic Geometry. Volume 10 of Algorithms and Computations in Mathematics","author":"S Basu","year":"2006","unstructured":"Basu, S., Pollack, R., Roy, M.E.: Algorithms in Real Algebraic Geometry. Volume 10 of Algorithms and Computations in Mathematics. Springer, Berlin (2006)"},{"key":"394_CR7","first-page":"272","volume-title":"EUROCAL \u201985, Volume 204 of Lecture Notes in Computer Science","author":"W B\u00f6ge","year":"1985","unstructured":"B\u00f6ge, W., Gebauer, R., Kredel, H.: Gr\u00f6bner bases using SAC2. In: Caviness, B.F. (ed.) EUROCAL \u201985, Volume 204 of Lecture Notes in Computer Science, pp. 272\u2013274. Springer, Berlin (1985)"},{"key":"394_CR8","doi-asserted-by":"crossref","unstructured":"Boser, B.E., Guyon, I.M., Vapnik, V.N.: A training algorithm for optimal margin classifiers. In: Proceedings of the Fifth Annual Workshop on Computational Learning Theory, COLT \u201992, pp. 144\u2013152. ACM (1992)","DOI":"10.1145\/130385.130401"},{"key":"394_CR9","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":"394_CR10","first-page":"44","volume-title":"Computer Algebra in Scientific Computing, Volume 8660 of Lecture Notes in Computer Science","author":"R Bradford","year":"2014","unstructured":"Bradford, R., Chen, C., Davenport, J.H., England, M., Moreno Maza, M., Wilson, D.: Truth table invariant cylindrical algebraic decomposition by regular chains. In: Gerdt, V.P., Koepf, W., Seiler, W.M., Vorozhtsov, E.V. (eds.) Computer Algebra in Scientific Computing, Volume 8660 of Lecture Notes in Computer Science, pp. 44\u201358. Springer, Berlin (2014)"},{"key":"394_CR11","doi-asserted-by":"crossref","unstructured":"Bradford, R., Davenport, J.H., England, M., Errami, H., Gerdt, V., Grigoriev, D., Hoyt, C., Ko\u0161ta, M., Radulescu, O., Sturm, T., Weber, A.: A case study on the parametric occurrence of multiple steady states. In: Proceedings of the 2017 ACM International Symposium on Symbolic and Algebraic Computation, ISSAC \u201917, pp. 45\u201352. ACM (2017)","DOI":"10.1145\/3087604.3087622"},{"key":"394_CR12","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 38th International Symposium on Symbolic and Algebraic Computation, ISSAC \u201913, pp. 125\u2013132. ACM (2013)","DOI":"10.1145\/2465506.2465516"},{"key":"394_CR13","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.jsc.2015.11.002","volume":"76","author":"R Bradford","year":"2016","unstructured":"Bradford, R., Davenport, J.H., England, M., McCallum, S., Wilson, D.: Truth table invariant cylindrical algebraic decomposition. J. Symb. Comput. 76, 1\u201335 (2016)","journal-title":"J. Symb. Comput."},{"key":"394_CR14","first-page":"19","volume-title":"Intelligent Computer Mathematics, Volume 7961 of Lecture Notes in Computer Science","author":"R Bradford","year":"2013","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. (eds.) Intelligent Computer Mathematics, Volume 7961 of Lecture Notes in Computer Science, pp. 19\u201334. Springer, Berlin (2013)"},{"key":"394_CR15","unstructured":"Bridge, J.P.: Machine learning and automated theorem proving. Technical Report UCAM-CL-TR-792, University of Cambridge, Computer Laboratory (2010)"},{"key":"394_CR16","unstructured":"Bridge, J.P., Holden, S.B., Paulson, L.C.: Machine learning for first-order theorem proving. J. Autom. Reason. 1\u201332 (2014)"},{"issue":"5","key":"394_CR17","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1006\/jsco.2001.0463","volume":"32","author":"CW 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":"394_CR18","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1145\/968708.968710","volume":"37","author":"CW Brown","year":"2003","unstructured":"Brown, C.W.: 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":"394_CR19","unstructured":"Brown, C.W.: Companion to the tutorial: cylindrical algebraic decomposition. Presented at ISSAC \u201904 (2004). http:\/\/www.usna.edu\/Users\/cs\/wcbrown\/research\/ISSAC04\/handout.pdf"},{"key":"394_CR20","doi-asserted-by":"crossref","unstructured":"Brown, C.W.: Open non-uniform cylindrical algebraic decompositions. In: Proceedings of the 2015 International Symposium on Symbolic and Algebraic Computation, ISSAC \u201915, pp. 85\u201392. ACM (2015)","DOI":"10.1145\/2755996.2756654"},{"key":"394_CR21","doi-asserted-by":"crossref","unstructured":"Brown, C.W., Davenport, J.H.: The complexity of quantifier elimination and cylindrical algebraic decomposition. In: Proceedings of the 2007 International Symposium on Symbolic and Algebraic Computation, ISSAC \u201907, pp. 54\u201360. ACM (2007)","DOI":"10.1145\/1277548.1277557"},{"key":"394_CR22","doi-asserted-by":"crossref","first-page":"1157","DOI":"10.1016\/j.jsc.2005.09.011","volume":"41","author":"CW 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":"394_CR23","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1016\/j.jsc.2014.09.024","volume":"70","author":"CW Brown","year":"2015","unstructured":"Brown, C.W., Kosta, M.: Constructing a single cell in cylindrical algebraic decomposition. J. Symb. Comput. 70, 14\u201348 (2015)","journal-title":"J. Symb. Comput."},{"issue":"3\u20134","key":"394_CR24","doi-asserted-by":"crossref","first-page":"475","DOI":"10.1016\/j.jsc.2005.09.007","volume":"41","author":"B Buchberger","year":"2006","unstructured":"Buchberger, B.: Bruno Buchberger\u2019s Ph.D. thesis (1965): an algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. J. Symb. Comput. 41(3\u20134), 475\u2013511 (2006)","journal-title":"J. Symb. Comput."},{"key":"394_CR25","unstructured":"Buchberger, B., Hong, H.: Speeding up quantifier elimination by Gr\u00f6bner bases. Technical report, 91-06. RISC, Johannes Kepler University (1991)"},{"issue":"03","key":"394_CR26","doi-asserted-by":"crossref","first-page":"459","DOI":"10.1142\/S0218001403002460","volume":"17","author":"H Byun","year":"2003","unstructured":"Byun, H., Lee, S.: A survey on pattern recognition applications of support vector machines. Int. J. Pattern Recognit. Artif. Intell. 17(03), 459\u2013486 (2003)","journal-title":"Int. J. Pattern Recognit. Artif. Intell."},{"key":"394_CR27","doi-asserted-by":"crossref","unstructured":"Carette, J.: Understanding expression simplification. In: Proceedings of the 2004 International Symposium on Symbolic and Algebraic Computation, ISSAC \u201904, pp. 72\u201379. ACM (2004)","DOI":"10.1145\/1005285.1005298"},{"key":"394_CR28","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-7091-9459-1","volume-title":"Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation","author":"B Caviness","year":"1998","unstructured":"Caviness, B., Johnson, J.: Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation. Springer, Berlin (1998)"},{"issue":"1","key":"394_CR29","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/s00419-017-1271-8","volume":"88","author":"AE Charalampakis","year":"2018","unstructured":"Charalampakis, A.E., Chatzigiannelis, I.: Analytical solutions for the minimum weight design of trusses by cylindrical algebraic decomposition. Arch. Appl. Mech. 88(1), 39\u201349 (2018)","journal-title":"Arch. Appl. Mech."},{"key":"394_CR30","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1007\/978-3-662-43799-5_17","volume-title":"Computer Mathematics","author":"C Chen","year":"2014","unstructured":"Chen, C., Moreno Maza, M.: An incremental algorithm for computing cylindrical algebraic decompositions. In: Feng, R., Lee, W., Sato, Y. (eds.) Computer Mathematics, pp. 199\u2013221. Springer, Berlin (2014)"},{"key":"394_CR31","first-page":"283","volume-title":"Mathematical Software\u2014ICMS 2014, Volume 8592 of Lecture Notes in Computer Science","author":"C Chen","year":"2014","unstructured":"Chen, C., Moreno Maza, M.: Real quantifier elimination in the RegularChains library. In: Hong, H., Yap, C. (eds.) Mathematical Software\u2014ICMS 2014, Volume 8592 of Lecture Notes in Computer Science, pp. 283\u2013290. Springer, Heidelberg (2014)"},{"key":"394_CR32","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1016\/j.jsc.2015.11.008","volume":"75","author":"C Chen","year":"2016","unstructured":"Chen, C., Moreno Maza, M.: Quantifier elimination by cylindrical algebraic decomposition based on regular chains. Journal of Symbolic Computation 75, 74\u201393 (2016)","journal-title":"Journal of Symbolic Computation"},{"key":"394_CR33","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 2009 International Symposium on Symbolic and Algebraic Computation, ISSAC \u201909, pp. 95\u2013102. ACM (2009)","DOI":"10.1145\/1576702.1576718"},{"key":"394_CR34","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 (reprinted in the collection [28]) (1975)","DOI":"10.1007\/3-540-07407-4_17"},{"key":"394_CR35","first-page":"34","volume-title":"EUROCAL \u201985, Volume 204 of Lecture Notes in Computer Science","author":"GE Collins","year":"1985","unstructured":"Collins, G.E.: The SAC-2 computer algebra system. In: Caviness, B.F. (ed.) EUROCAL \u201985, Volume 204 of Lecture Notes in Computer Science, pp. 34\u201335. Springer, Berlin (1985)"},{"key":"394_CR36","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1016\/S0747-7171(08)80152-6","volume":"12","author":"GE 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."},{"issue":"3","key":"394_CR37","first-page":"273","volume":"20","author":"C Cortes","year":"1995","unstructured":"Cortes, C., Vapnik, V.: Support-vector networks. Mach. Learn. 20(3), 273\u2013297 (1995)","journal-title":"Mach. Learn."},{"key":"394_CR38","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: 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC \u201912, pp. 83\u201388. IEEE (2012)","DOI":"10.1109\/SYNASC.2012.68"},{"key":"394_CR39","first-page":"157","volume-title":"Mathematical Software\u2014Proceedings of ICMS 2016, Volume 9725 of Lecture Notes in Computer Science","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.) Mathematical Software\u2014Proceedings of ICMS 2016, Volume 9725 of Lecture Notes in Computer Science, pp. 157\u2013164. Springer, Berlin (2016)"},{"issue":"1\u20132","key":"394_CR40","doi-asserted-by":"crossref","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)","journal-title":"J. Symb. Comput."},{"key":"394_CR41","doi-asserted-by":"crossref","unstructured":"Dolzmann, A., Seidl, A., Sturm, T.: Efficient projection orders for CAD. In: Proceedings of the 2004 International Symposium on Symbolic and Algebraic Computation, ISSAC \u201904, pp. 111\u2013118. ACM (2004)","DOI":"10.1145\/1005285.1005303"},{"key":"394_CR42","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/978-3-319-96418-8_20","volume-title":"Mathematical Software\u2014ICMS 2018, Volume 10931 of Lecture Notes in Computer Science","author":"M England","year":"2018","unstructured":"England, M.: Machine Learning for Mathematical Software. In: Davenport, J.H., Kauers, M., Labahn, G., Urban, J. (eds.) Mathematical Software\u2014ICMS 2018, Volume 10931 of Lecture Notes in Computer Science, pp. 165\u2013174. Springer, Heidelberg (2018)"},{"key":"394_CR43","first-page":"45","volume-title":"Intelligent Computer Mathematics, Volume 8543 of Lecture Notes in Artificial Intelligence","author":"M England","year":"2014","unstructured":"England, M., Bradford, R., Chen, C., Davenport, J.H., Moreno Maza, M., Wilson, D.: Problem formulation for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) Intelligent Computer Mathematics, Volume 8543 of Lecture Notes in Artificial Intelligence, pp. 45\u201360. Springer, Berlin (2014)"},{"key":"394_CR44","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 the 2015 International Symposium on Symbolic and Algebraic Computation, ISSAC \u201915, pp. 165\u2013172. ACM (2015)","DOI":"10.1145\/2755996.2756678"},{"key":"394_CR45","first-page":"136","volume-title":"Intelligent Computer Mathematics, Volume 7961 of Lecture Notes in Computer Science","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, Volume 7961 of Lecture Notes in Computer Science, pp. 136\u2013151. Springer, Berlin (2013)"},{"key":"394_CR46","first-page":"450","volume-title":"Mathematical Software\u2014ICMS 2014, Volume 8592 of Lecture Notes in Computer Science","author":"M England","year":"2014","unstructured":"England, M., Bradford, R., Davenport, J.H., Wilson, D.: Choosing a variable ordering for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition. In: Hong, H., Yap, C. (eds.) Mathematical Software\u2014ICMS 2014, Volume 8592 of Lecture Notes in Computer Science, pp. 450\u2013457. Springer, Heidelberg (2014)"},{"key":"394_CR47","doi-asserted-by":"crossref","unstructured":"England, M., Davenport, J.H.: The complexity of cylindrical algebraic decomposition with respect to polynomial degree. In: Gerdt, V.P., Koepf, W., Werner, W.M., Vorozhtsov, E.V. (eds.) Computer Algebra in Scientific Computing: 18th International Workshop, CASC 2016, Volume 9890 of Lecture Notes in Computer Science, pp. 172\u2013192. Springer (2016)","DOI":"10.1007\/978-3-319-45641-6_12"},{"key":"394_CR48","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-3-319-66320-3_8","volume-title":"Computer Algebra in Scientific Computing (CASC), Volume 10490 of Lecture Notes in Computer Science","author":"M England","year":"2017","unstructured":"England, M., Errami, H., Grigoriev, D., Radulescu, O., Sturm, T., Weber, A.: Symbolic versus numerical computation and visualization of parameter regions for multistationarity of biological networks. In: Gerdt, V.P., Koepf, W., Seiler, W.M., Vorozhtsov, E.V. (eds.) Computer Algebra in Scientific Computing (CASC), Volume 10490 of Lecture Notes in Computer Science, pp. 93\u2013108. Springer, Berlin (2017)"},{"key":"394_CR49","first-page":"458","volume-title":"Mathematical Software\u2014ICMS 2014, Volume 8592 of Lecture Notes in Computer Science","author":"M England","year":"2014","unstructured":"England, M., Wilson, D., Bradford, R., Davenport, J.H.: Using the regular chains library to build cylindrical algebraic decompositions by projecting and lifting. In: Hong, H., Yap, C. (eds.) Mathematical Software\u2014ICMS 2014, Volume 8592 of Lecture Notes in Computer Science, pp. 458\u2013465. Springer, Berlin (2014)"},{"key":"394_CR50","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1016\/j.jsc.2015.11.010","volume":"75","author":"M Erascu","year":"2016","unstructured":"Erascu, M., Hong, H.: Real quantifier elimination for the synthesis of optimal numerical algorithms (case study: square root computation). J. Symb. Comput. 75, 110\u2013126 (2016)","journal-title":"J. Symb. Comput."},{"key":"394_CR51","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/j.jcp.2015.02.050","volume":"291","author":"H Errami","year":"2015","unstructured":"Errami, H., Eiswirth, M., Grigoriev, D., Seiler, W.M., Sturm, T., Weber, A.: Detection of Hopf bifurcations in chemical reaction networks using convex coordinates. J. Comput. Phys. 291, 279\u2013302 (2015)","journal-title":"J. Comput. Phys."},{"key":"394_CR52","doi-asserted-by":"crossref","unstructured":"Faug\u00e8re, J.C.: A new efficient algorithm for computing Gr\u00f6bner bases without reduction to zero (F5). In: Proceedings of the 2002 International Symposium on Symbolic and Algebraic Computation, ISSAC \u201902, pp. 75\u201383. ACM (2002)","DOI":"10.1145\/780506.780516"},{"key":"394_CR53","unstructured":"Fayyad, U.M., Irani, K.B.: Multi-interval discretization of continuous-valued attributes for classification learning. In: Proceedings of the International Joint Conference on Uncertainty in AI, pp. 1022\u20131027. http:\/\/trs-new.jpl.nasa.gov\/dspace\/handle\/2014\/35171 (1993)"},{"key":"394_CR54","volume-title":"Machine Learning: Applications in Expert Systems and Information Retrieval","author":"R Forsyth","year":"1986","unstructured":"Forsyth, R., Rada, R.: Machine Learning: Applications in Expert Systems and Information Retrieval. Halsted Press, New York (1986)"},{"key":"394_CR55","unstructured":"Graebe, H.G., Nareike, A., Johanning, S.: The SymbolicData project: towards a computer algebra social network. In: England, M., Davenport, J.H., Kohlhase, A., Kohlhase, M., Libbrecht, P., Neuper, W., Quaresma, P., Sexton, A.P., Sojka, P., Urban, J., Watt, S.M. (eds.) Joint Proceedings of the MathUI, OpenMath and ThEdu Workshops and Work in Progress Track at CICM, Number 1186 in CEUR Workshop Proceedings (2014)"},{"key":"394_CR56","first-page":"1157","volume":"3","author":"I Guyon","year":"2003","unstructured":"Guyon, I., Elisseeff, A.: An introduction to variable and feature selection. J. Mach. Learn. Res. 3, 1157\u20131182 (2003)","journal-title":"J. Mach. Learn. Res."},{"issue":"1","key":"394_CR57","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1145\/1656274.1656278","volume":"11","author":"M Hall","year":"2009","unstructured":"Hall, M., Frank, E., Holmes, G., Pfahringer, B., Reutemann, P., Witten, I.H.: The WEKA data mining software: an update. SIGKDD Explor. Newsl. 11(1), 10\u201318 (2009)","journal-title":"SIGKDD Explor. Newsl."},{"key":"394_CR58","unstructured":"Hall, M.A.: Correlation-based feature selection for discrete and numeric class machine learning. In: Proceedings of the Seventeenth International Conference on Machine Learning, ICML \u201900, pp. 359\u2013366. Morgan Kaufmann Publishers Inc. (2000)"},{"issue":"6","key":"394_CR59","doi-asserted-by":"crossref","first-page":"1437","DOI":"10.1109\/TKDE.2003.1245283","volume":"15","author":"MA Hall","year":"2003","unstructured":"Hall, M.A., Holmes, G.: Benchmarking attribute selection techniques for discrete class data mining. IEEE Trans. Knowl. Data Eng. 15(6), 1437\u20131447 (2003)","journal-title":"IEEE Trans. Knowl. Data Eng."},{"key":"394_CR60","doi-asserted-by":"crossref","unstructured":"Han, J., Dai, L., Xia, B.: Constructing fewer open cells by gcd computation in CAD projection. In: Proceedings of the 39th International Symposium on Symbolic and Algebraic Computation, ISSAC \u201914, pp. 240\u2013247. ACM (2014)","DOI":"10.1145\/2608628.2608676"},{"issue":"1","key":"394_CR61","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2768577.2768578","volume":"49","author":"A Heinle","year":"2015","unstructured":"Heinle, A., Levandovskyy, V.: The SDEval benchmarking toolkit. ACM Commun. Comput. Algebra 49(1), 1\u20139 (2015)","journal-title":"ACM Commun. Comput. Algebra"},{"key":"394_CR62","doi-asserted-by":"crossref","unstructured":"Hong, H.: An improvement of the projection operator in cylindrical algebraic decomposition. In: Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC \u201990, pp. 261\u2013264. ACM (1990)","DOI":"10.1145\/96877.96943"},{"key":"394_CR63","unstructured":"Hong, H.: Comparison of several decision algorithms for the existential theory of the reals. Technical report, RISC, Linz (1991)"},{"issue":"5","key":"394_CR64","doi-asserted-by":"crossref","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 Netw. 2(5), 359\u2013366 (1989)","journal-title":"Neural Netw."},{"key":"394_CR65","unstructured":"Hsu, C., Chang, C., Lin, C.: A practical guide to support vector classification. Technical report, Department of Computer Science, National Taiwan University (2003)"},{"key":"394_CR66","doi-asserted-by":"crossref","unstructured":"Huang, Z., England, M., Davenport, J.H., Paulson, L.: Using machine learning to decide when to precondition cylindrical algebraic decomposition with Groebner bases. In: 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC \u201916), pp. 45\u201352. IEEE (2016)","DOI":"10.1109\/SYNASC.2016.020"},{"key":"394_CR67","first-page":"92","volume-title":"Intelligent Computer Mathematics, Volume 8543 of Lecture Notes in Artificial Intelligence","author":"Z Huang","year":"2014","unstructured":"Huang, Z., England, M., Wilson, D., Davenport, J.H., Paulson, L., Bridge, J.: Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) Intelligent Computer Mathematics, Volume 8543 of Lecture Notes in Artificial Intelligence, pp. 92\u2013107. Springer, Berlin (2014)"},{"key":"394_CR68","unstructured":"Huang, Z., Paulson, L.: An application of machine learning to RCF decision procedures. In: 20th Automated Reasoning Workshop, University of Dundee, UK, ARW \u201913 (2013)"},{"key":"394_CR69","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 2009 Conference on Symbolic Numeric Computation, SNC \u201909, pp. 55\u201364 (2009)","DOI":"10.1145\/1577190.1577203"},{"key":"394_CR70","first-page":"169","volume-title":"Advances in Kernel Methods","author":"T Joachims","year":"1999","unstructured":"Joachims, T.: Making large-scale support vector machine learning practical. In: Sch\u00f6lkopf, B., Burges, C.J.C., Smola, A.J. (eds.) Advances in Kernel Methods, pp. 169\u2013184. MIT Press, Cambridge (1999)"},{"key":"394_CR71","doi-asserted-by":"crossref","unstructured":"Joachims, T.: A support vector method for multivariate performance measures. In: Proceedings of the 22nd International Conference on Machine Learning, ICML \u201905, pp. 377\u2013384. ACM (2005)","DOI":"10.1145\/1102351.1102399"},{"key":"394_CR72","doi-asserted-by":"crossref","unstructured":"Jovanovic, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Automated Reasoning: 6th International Joint Conference (IJCAR), Volume 7364 of Lecture Notes in Computer Science, pp. 339\u2013354. Springer (2012)","DOI":"10.1007\/978-3-642-31365-3_27"},{"key":"394_CR73","first-page":"236","volume-title":"Mathematical Aspects of Computer and Information Sciences (MACIS \u201915), Volume 9582 of Lecture Notes in Computer Science","author":"M Kobayashi","year":"2016","unstructured":"Kobayashi, M., Iwane, H., Matsuzaki, T., Anai, H.: Efficient subformula orders for real quantifier elimination of non-prenex formulas. In: Kotsireas, S.I., Rump, M.S., Yap, K.C. (eds.) Mathematical Aspects of Computer and Information Sciences (MACIS \u201915), Volume 9582 of Lecture Notes in Computer Science, pp. 236\u2013251. Springer, Berlin (2016)"},{"issue":"2","key":"394_CR74","doi-asserted-by":"crossref","first-page":"442","DOI":"10.1016\/0005-2795(75)90109-9","volume":"405","author":"BW Matthews","year":"1975","unstructured":"Matthews, B.W.: Comparison of the predicted and observed secondary structure of T4 phage lysozyme. Biochim. Biophys. Acta (BBA) Protein Struct. 405(2), 442\u2013451 (1975)","journal-title":"Biochim. Biophys. Acta (BBA) Protein Struct."},{"issue":"3","key":"394_CR75","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1016\/0001-8708(82)90048-2","volume":"46","author":"EW Mayr","year":"1982","unstructured":"Mayr, E.W., Meyer, A.R.: The complexity of the word problems for commutative semigroups and polynomial ideals. Adv. Math. 46(3), 305\u2013329 (1982)","journal-title":"Adv. Math."},{"key":"394_CR76","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1007\/978-3-7091-9459-1_12","volume-title":"Quantifier Elimination and Cylindrical Algebraic Decomposition, Texts and Monographs in Symbolic Computation","author":"S McCallum","year":"1998","unstructured":"McCallum, S.: An improved projection operation for cylindrical algebraic decomposition. In: Caviness, B., Johnson, J. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition, Texts and Monographs in Symbolic Computation, pp. 242\u2013268. Springer, Berlin (1998)"},{"key":"394_CR77","doi-asserted-by":"crossref","unstructured":"McCallum, S.: On projection in CAD-based quantifier elimination with equational constraint. In: Proceedings of the 1999 International Symposium on Symbolic and Algebraic Computation, ISSAC \u201999, pp. 145\u2013149. ACM (1999)","DOI":"10.1145\/309831.309892"},{"key":"394_CR78","doi-asserted-by":"crossref","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)","journal-title":"J. Symb. Comput."},{"issue":"4","key":"394_CR79","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/BF02478259","volume":"5","author":"WS McCulloch","year":"1943","unstructured":"McCulloch, W.S., Pitts, W.: A logical calculus of the ideas immanent in nervous activity. Bull. Math. Biophys. 5(4), 115\u2013133 (1943)","journal-title":"Bull. Math. Biophys."},{"key":"394_CR80","doi-asserted-by":"crossref","unstructured":"Mulligan, C.B.: Automated economic reasoning with quantifier elimination. Working Paper 22922, National Bureau of Economic Research (2016)","DOI":"10.3386\/w22922"},{"key":"394_CR81","first-page":"1","volume":"2","author":"BR Patel","year":"2014","unstructured":"Patel, B.R., Kaushik, K.R.: A survey on decision tree algorithm for classification. Int. J. Eng. Dev. Res. 2, 1\u20135 (2014)","journal-title":"Int. J. Eng. Dev. Res."},{"key":"394_CR82","first-page":"1","volume-title":"Interactive Theorem Proving, Volume 7406 of Lecture Notes in Computer Science","author":"LC Paulson","year":"2012","unstructured":"Paulson, L.C.: Metitarski: past and future. In: Beringer, L., Felty, A. (eds.) Interactive Theorem Proving, Volume 7406 of Lecture Notes in Computer Science, pp. 1\u201310. Springer, Berlin (2012)"},{"key":"394_CR83","first-page":"171","volume-title":"Automated Reasoning, Volume 5195 of Lecture Notes in Computer Science","author":"A Platzer","year":"2008","unstructured":"Platzer, A., Quesel, J.D.: KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning, Volume 5195 of Lecture Notes in Computer Science, pp. 171\u2013178. Springer, Berlin (2008)"},{"key":"394_CR84","first-page":"485","volume-title":"Automated Deduction (CADE-22), Volume 5663 of Lecture Notes in Computer Science","author":"A Platzer","year":"2009","unstructured":"Platzer, A., Quesel, J.D., R\u00fcmmer, P.: Real world verification. In: Schmidt, R.A. (ed.) Automated Deduction (CADE-22), Volume 5663 of Lecture Notes in Computer Science, pp. 485\u2013501. Springer, Berlin (2009)"},{"key":"394_CR85","volume-title":"Numerical Recipes in C (2nd Ed.): The Art of Scientific Computing","author":"WH Press","year":"1992","unstructured":"Press, W.H., Teukolsky, S.A., Vetterling, W.T., Flannery, B.P.: Numerical Recipes in C (2nd Ed.): The Art of Scientific Computing. Cambridge University Press, Cambridge (1992)"},{"issue":"1","key":"394_CR86","first-page":"81","volume":"1","author":"JR Quinlan","year":"1986","unstructured":"Quinlan, J.R.: Induction of decision trees. Mach. Learn. 1(1), 81\u2013106 (1986)","journal-title":"Mach. Learn."},{"issue":"6","key":"394_CR87","doi-asserted-by":"crossref","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. Psychol. Rev. 65(6), 386 (1958)","journal-title":"Psychol. Rev."},{"key":"394_CR88","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/4057.001.0001","volume-title":"Kernel methods in computational biology","author":"B Sch\u00f6lkopf","year":"2004","unstructured":"Sch\u00f6lkopf, B., Tsuda, K., Vert, J.-P.: Kernel methods in computational biology. MIT Press, Cambridge (2004)"},{"issue":"1","key":"394_CR89","doi-asserted-by":"crossref","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 Comput. Surv. 34(1), 1\u201347 (2002)","journal-title":"ACM Comput. Surv."},{"issue":"1","key":"394_CR90","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1145\/584091.584093","volume":"5","author":"Claude E Shannon","year":"2001","unstructured":"Shannon, Claude E.: A mathematical theory of communication. Mob. Comput. Commun. Rev. 5(1), 3\u201355 (2001)","journal-title":"Mob. Comput. Commun. Rev."},{"key":"394_CR91","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511809682","volume-title":"Kernel Methods for Pattern Analysis","author":"J Shawe-Taylor","year":"2004","unstructured":"Shawe-Taylor, J., Cristianini, N.: Kernel Methods for Pattern Analysis. Cambridge University Press, Cambridge (2004)"},{"issue":"3","key":"394_CR92","doi-asserted-by":"crossref","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. Auton. Robot. 8(3), 345\u2013383 (2000)","journal-title":"Auton. Robot."},{"issue":"9","key":"394_CR93","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":"394_CR94","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1016\/j.jsc.2015.11.018","volume":"76","author":"A Strzebo\u0144ski","year":"2016","unstructured":"Strzebo\u0144ski, A.: Cylindrical algebraic decomposition using local projections. J. Symb. Comput. 76, 36\u201364 (2016)","journal-title":"J. Symb. Comput."},{"key":"394_CR95","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry. RAND Corporation, Santa Monica, CA (reprinted in the collection [28]) (1948)"},{"issue":"1","key":"394_CR96","first-page":"821","volume":"25","author":"VN Vapnik","year":"1964","unstructured":"Vapnik, V.N., Chervonenkis, A.Y.: A note on one class of perceptrons. Autom. Remote Control 25(1), 821\u2013837 (1964)","journal-title":"Autom. Remote Control"},{"key":"394_CR97","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/s11786-014-0191-z","volume":"8","author":"D Wilson","year":"2014","unstructured":"Wilson, D., Bradford, R., Davenport, J.H., England, M.: Cylindrical algebraic sub-decompositions. Math. Comput. Sci. 8, 263\u2013288 (2014)","journal-title":"Math. Comput. Sci."},{"key":"394_CR98","unstructured":"Wilson, D., Davenport, J.H., England, M., Bradford, R.: A \u201cpiano movers\u201d problem reformulated. In: 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC \u201913, pp. 53\u201360. IEEE (2013)"},{"key":"394_CR99","doi-asserted-by":"crossref","unstructured":"Wilson, D., England, M., Davenport, J.H., Bradford, R.: Using the distribution of cells by dimension in a cylindrical algebraic decomposition. In: 16th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC \u201914, pp. 53\u201360. IEEE (2014)","DOI":"10.1109\/SYNASC.2014.15"},{"issue":"3","key":"394_CR100","first-page":"67","volume":"46","author":"DJ Wilson","year":"2012","unstructured":"Wilson, D.J., Bradford, R.J., Davenport, J.H.: A repository for CAD examples. ACM Commun. Comput. Algebra 46(3), 67\u201369 (2012)","journal-title":"ACM Commun. Comput. Algebra"},{"key":"394_CR101","first-page":"280","volume-title":"Intelligent Computer Mathematics, Volume 7362 of Lecture Notes in Computer Science","author":"DJ 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., Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) Intelligent Computer Mathematics, Volume 7362 of Lecture Notes in Computer Science, pp. 280\u2013294. Springer, Berlin (2012)"}],"container-title":["Mathematics in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11786-019-00394-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11786-019-00394-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11786-019-00394-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,15]],"date-time":"2023-09-15T10:46:57Z","timestamp":1694774817000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11786-019-00394-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,4,3]]},"references-count":101,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2019,12]]}},"alternative-id":["394"],"URL":"https:\/\/doi.org\/10.1007\/s11786-019-00394-8","relation":{},"ISSN":["1661-8270","1661-8289"],"issn-type":[{"value":"1661-8270","type":"print"},{"value":"1661-8289","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,4,3]]},"assertion":[{"value":"31 January 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 May 2018","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 February 2019","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 April 2019","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}