{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T06:31:46Z","timestamp":1762324306420,"version":"3.37.3"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319964171"},{"type":"electronic","value":"9783319964188"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-96418-8_20","type":"book-chapter","created":{"date-parts":[[2018,7,13]],"date-time":"2018-07-13T06:57:13Z","timestamp":1531465033000},"page":"165-174","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Machine Learning for Mathematical Software"],"prefix":"10.1007","author":[{"given":"Matthew","family":"England","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,14]]},"reference":[{"key":"20_CR1","unstructured":"Alemi, A., Chollet, F., Een, N., Irving, G., Szegedy, C., Urban, J.: DeepMath - deep sequence models for premise selection. In: Proceedings 30th International Conference on Neural Information Processing Systems (NIPS 2016), pp. 2243\u20132251. Curran Associates Inc. (2016)"},{"key":"20_CR2","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 J. Comput. 13, 865\u2013877 (1984). https:\/\/doi.org\/10.1137\/0213054","journal-title":"SIAM J. Comput."},{"key":"20_CR3","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T.: Handbook of Satisfiability, vol. 185. Frontiers in Artificial Intelligence and Applications. IOS Press (2009)"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Bradford, R., Davenport, J., 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 2017 ACM International Symposium on Symbolic and Algebraic Computation (ISSAC 2017), pp. 45\u201352. ACM (2017). https:\/\/doi.org\/10.1145\/3087604.3087622","DOI":"10.1145\/3087604.3087622"},{"key":"20_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jsc.2015.11.002","volume":"76","author":"R Bradford","year":"2016","unstructured":"Bradford, R., Davenport, J., England, M., McCallum, S., Wilson, D.: Truth table invariant cylindrical algebraic decomposition. J. Symbolic Comput. 76, 1\u201335 (2016). https:\/\/doi.org\/10.1016\/j.jsc.2015.11.002","journal-title":"J. Symbolic Comput."},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","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. 7961, pp. 19\u201334. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39320-4_2"},{"issue":"2","key":"20_CR7","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/s10817-014-9301-5","volume":"53","author":"J Bridge","year":"2014","unstructured":"Bridge, J., Holden, S., Paulson, L.: Machine learning for first-order theorem proving. J. Autom. Reasoning 53(2), 141\u2013172 (2014). https:\/\/doi.org\/10.1007\/s10817-014-9301-5","journal-title":"J. Autom. Reasoning"},{"key":"20_CR8","unstructured":"Brown, C.: Companion to the tutorial: cylindrical algebraic decomposition. In: Presented at ISSAC 2004 (2004). http:\/\/www.usna.edu\/Users\/cs\/wcbrown\/research\/ISSAC04\/handout.pdf"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Brown, C., Davenport, J.: The complexity of quantifier elimination and cylindrical algebraic decomposition. In: Proceedings of 2007 International Symposium on Symbolic and Algebraic Computation (ISSAC 2007), pp. 54\u201360. ACM (2007). https:\/\/doi.org\/10.1145\/1277548.1277557","DOI":"10.1145\/1277548.1277557"},{"key":"20_CR10","unstructured":"Buchberger, B., Hong, H.: Speeding up quantifier elimination by Gr\u00f6bner bases. Technical report, 91\u201306. RISC, Johannes Kepler University (1991)"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Carette, J.: Understanding expression simplification. In: Proceedings of the 2004 International Symposium on Symbolic and Algebraic Computation (ISSAC 2004), pp. 72\u201379. ACM (2004). https:\/\/doi.org\/10.1145\/1005285.1005298","DOI":"10.1145\/1005285.1005298"},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-02614-0_21","volume-title":"Intelligent Computer Mathematics","author":"J Carette","year":"2009","unstructured":"Carette, J., Farmer, W.M.: A review of mathematical knowledge management. In: Carette, J., Dixon, L., Coen, C.S., Watt, S.M. (eds.) CICM 2009. LNCS (LNAI), vol. 5625, pp. 233\u2013246. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02614-0_21"},{"issue":"3","key":"20_CR13","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1023\/A:1022627411411","volume":"20","author":"C Cortes","year":"1995","unstructured":"Cortes, C., Vapnik, V.: Support-vector networks. Mach. Learn. 20(3), 273\u2013297 (1995). https:\/\/doi.org\/10.1023\/A:1022627411411","journal-title":"Mach. Learn."},{"key":"20_CR14","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: 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2012, pp. 83\u201388. IEEE (2012). https:\/\/doi.org\/10.1109\/SYNASC.2012.68","DOI":"10.1109\/SYNASC.2012.68"},{"issue":"1\u20132","key":"20_CR15","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S0747-7171(88)80004-X","volume":"5","author":"J Davenport","year":"1988","unstructured":"Davenport, J., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symbolic Comput. 5(1\u20132), 29\u201335 (1988). https:\/\/doi.org\/10.1016\/S0747-7171(88)80004-X","journal-title":"J. Symbolic Comput."},{"key":"20_CR16","doi-asserted-by":"crossref","unstructured":"Dolzmann, A., Seidl, A., Sturm, T.: Efficient projection orders for CAD. In: Proceedings of 2004 International Symposium on Symbolic and Algebraic Computation (ISSAC 2004), pp. 111\u2013118. ACM (2004). https:\/\/doi.org\/10.1145\/1005285.1005303","DOI":"10.1145\/1005285.1005303"},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-319-08434-3_5","volume-title":"Intelligent Computer Mathematics","author":"M England","year":"2014","unstructured":"England, M., et al.: 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.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 45\u201360. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08434-3_5"},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"England, M., Bradford, R., Davenport, J.: Improving the use of equational constraints in cylindrical algebraic decomposition. In: Proceedings of 2015 International Symposium on Symbolic and Algebraic Computation (ISSAC 2015), pp. 165\u2013172. ACM (2015). https:\/\/doi.org\/10.1145\/2755996.2756678","DOI":"10.1145\/2755996.2756678"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-319-45641-6_12","volume-title":"Computer Algebra in Scientific Computing","author":"M England","year":"2016","unstructured":"England, M., Davenport, J.H.: The complexity of cylindrical algebraic decomposition with respect to polynomial degree. In: Gerdt, V.P., Koepf, W., Seiler, W.M., Vorozhtsov, E.V. (eds.) CASC 2016. LNCS, vol. 9890, pp. 172\u2013192. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-45641-6_12"},{"key":"20_CR20","doi-asserted-by":"crossref","unstructured":"Fukasaku, R., Iwane, H., Sato, Y.: Real quantifier elimination by computation of comprehensive Gr\u00f6bner systems. In: Proceedings of 2015 International Symposium on Symbolic and Algebraic Computation (ISSAC 2015), pp. 173\u2013180. ACM (2015). https:\/\/doi.org\/10.1145\/2755996.2756646","DOI":"10.1145\/2755996.2756646"},{"issue":"4","key":"20_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3092566","volume":"50","author":"Seyed Mohammad Ghaffarian","year":"2017","unstructured":"Ghaffarian, S., Shahriari, H.: Software vulnerability analysis and discovery using machine-learning and data-mining techniques: a survey. ACM Comput. Surv. 50(4) (2017). 36 pages, Article no. 56, https:\/\/doi.org\/10.1145\/3092566","journal-title":"ACM Computing Surveys"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Huang, Z., England, M., Davenport, J., 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 2016), pp. 45\u201352. IEEE (2016). https:\/\/doi.org\/10.1109\/SYNASC.2016.020","DOI":"10.1109\/SYNASC.2016.020"},{"key":"20_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-319-08434-3_8","volume-title":"Intelligent Computer Mathematics","author":"Z Huang","year":"2014","unstructured":"Huang, Z., et al.: 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.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 92\u2013107. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08434-3_8"},{"key":"20_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-319-32859-1_21","volume-title":"Mathematical Aspects of Computer and Information Sciences","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, I.S., Rump, S.M., Yap, C.K. (eds.) MACIS 2015. LNCS, vol. 9582, pp. 236\u2013251. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-32859-1_21"},{"key":"20_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-39634-2_6","volume-title":"Interactive Theorem Proving","author":"D K\u00fchlwein","year":"2013","unstructured":"K\u00fchlwein, D., Blanchette, J.C., Kaliszyk, C., Urban, J.: MaSh: machine learning for Sledgehammer. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 35\u201350. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_6"},{"key":"20_CR26","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-642-31365-3_30","volume-title":"Automated Reasoning","author":"D K\u00fchlwein","year":"2012","unstructured":"K\u00fchlwein, D., van Laarhoven, T., Tsivtsivadze, E., Urban, J., Heskes, T.: Overview and evaluation of premise selection techniques for large theory mathematics. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 378\u2013392. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_30"},{"key":"20_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-319-66263-3_8","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2017","author":"JH Liang","year":"2017","unstructured":"Liang, J.H., V.K., H.G., Poupart, P., Czarnecki, K., Ganesh, V.: An empirical study of branching heuristics through the lens of global learning rate. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 119\u2013135. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66263-3_8"},{"key":"20_CR28","doi-asserted-by":"crossref","unstructured":"McCallum, S.: On projection in CAD-based quantifier elimination with equational constraint. In: Proceedings of 1999 International Symposium on Symbolic and Algebraic Computation (ISSAC 1999), pp. 145\u2013149. ACM (1999). https:\/\/doi.org\/10.1145\/309831.309892","DOI":"10.1145\/309831.309892"},{"key":"20_CR29","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/978-3-319-08434-3_16","volume-title":"Intelligent Computer Mathematics","author":"U Sch\u00f6neberg","year":"2014","unstructured":"Sch\u00f6neberg, U., Sperber, W.: POS tagging and its applications for mathematics. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 213\u2013223. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08434-3_16"},{"key":"20_CR30","doi-asserted-by":"crossref","unstructured":"Seshia, S., Lahiri, S., Bryant, R.: A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. In: Proceedings of 2003 Design Automation Conference, pp. 425\u2013430 (2003). https:\/\/doi.org\/10.1145\/775832.775945","DOI":"10.1145\/775832.775945"},{"key":"20_CR31","doi-asserted-by":"crossref","unstructured":"Shawe-Taylor, J., Cristianini, N.: Kernel methods for pattern analysis. CUP (2004)","DOI":"10.1017\/CBO9780511809682"},{"issue":"7","key":"20_CR32","doi-asserted-by":"publisher","first-page":"859","DOI":"10.1016\/j.jsc.2010.08.017","volume":"46","author":"D Stoutemyer","year":"2011","unstructured":"Stoutemyer, D.: Ten commandments for good default expression simplification. J. Symbolic Comput. 46(7), 859\u2013887 (2011). https:\/\/doi.org\/10.1016\/j.jsc.2010.08.017","journal-title":"J. Symbolic Comput."},{"issue":"3","key":"20_CR33","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/s11786-017-0319-z","volume":"11","author":"T Sturm","year":"2017","unstructured":"Sturm, T.: A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications. Math. Comp. Sci. 11(3), 483\u2013502 (2017). https:\/\/doi.org\/10.1007\/s11786-017-0319-z","journal-title":"Math. Comp. Sci."},{"key":"20_CR34","unstructured":"Urban, J.: MaLARea: a metasystem for automated reasoning in large theories. In: Empirically Successful Automated Reasoning in Large Theories (ESARLT 2007), CEUR Workshop Proceedings, vol. 257, 14 pages. CEUR-WS (2007)"},{"key":"20_CR35","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/978-3-540-85110-3_44","volume-title":"Intelligent Computer Mathematics","author":"R \u0158eh\u016f\u0159ek","year":"2008","unstructured":"\u0158eh\u016f\u0159ek, R., Sojka, P.: Automated classification and categorization of mathematical knowledge. In: Autexier, S., et al. (eds.) CICM 2008. LNCS (LNAI), vol. 5144, pp. 543\u2013557. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-85110-3_44"},{"key":"20_CR36","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-642-31374-5_19","volume-title":"Intelligent Computer Mathematics","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., et al. (eds.) CICM 2012. LNCS (LNAI), vol. 7362, pp. 280\u2013294. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31374-5_19"},{"key":"20_CR37","doi-asserted-by":"crossref","unstructured":"Wu, H.: Improving SAT-solving with machine learning. In: Proceedings of the 2017 ACM SIGCSE Technical Symposium Computer Science Education, pp. 787\u2013788. ACM (2017). https:\/\/doi.org\/10.1145\/3017680.3022464","DOI":"10.1145\/3017680.3022464"},{"key":"20_CR38","doi-asserted-by":"crossref","first-page":"565","DOI":"10.1613\/jair.2490","volume":"32","author":"L Xu","year":"2008","unstructured":"Xu, L., Hutter, F., Hoos, H., Leyton-Brown, K.: SATzilla: portfolio-based algorithm selection for SAT. J. Artif. Intell. Res. 32, 565\u2013606 (2008)","journal-title":"J. Artif. Intell. Res."},{"issue":"2","key":"20_CR39","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3057270","volume":"50","author":"Ali Yadollahi","year":"2017","unstructured":"Yadollahi, A., Shahraki, A., Zaiane, O.: Current state of text sentiment analysis from opinion to emotion mining. ACM Comput. Surv. 50(2) (2017). 33 pages, Article no. 25, https:\/\/doi.org\/10.1145\/3057270","journal-title":"ACM Computing Surveys"},{"issue":"3","key":"20_CR40","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3068287","volume":"50","author":"Kok-Lim Alvin Yau","year":"2017","unstructured":"Yau, K.L., Qadir, J., Khoo, H., Ling, M., Komisarczuk, P.: A survey on reinforcement learning models and algorithms for traffic signal control. ACM Comput. Surv. 50(3) (2017). 38 pages, Article no. 34, https:\/\/doi.org\/10.1145\/3068287","journal-title":"ACM Computing Surveys"},{"issue":"2","key":"20_CR41","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1109\/TAI.2002.1180784","volume":"11","author":"D Zhang","year":"2003","unstructured":"Zhang, D., Tsai, J.: Machine learning and software engineering. Software Qual. J. 11(2), 87\u2013119 (2003). https:\/\/doi.org\/10.1109\/TAI.2002.1180784","journal-title":"Software Qual. J."}],"container-title":["Lecture Notes in Computer Science","Mathematical Software \u2013 ICMS 2018"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-96418-8_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T15:35:45Z","timestamp":1571585745000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-96418-8_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319964171","9783319964188"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-96418-8_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}