{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T02:04:18Z","timestamp":1760061858189,"version":"3.40.3"},"publisher-location":"Cham","reference-count":11,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319328584"},{"type":"electronic","value":"9783319328591"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-32859-1_21","type":"book-chapter","created":{"date-parts":[[2016,4,15]],"date-time":"2016-04-15T15:12:06Z","timestamp":1460733126000},"page":"236-251","source":"Crossref","is-referenced-by-count":7,"title":["Efficient Subformula Orders for Real Quantifier Elimination of Non-prenex Formulas"],"prefix":"10.1007","author":[{"given":"Munehiro","family":"Kobayashi","sequence":"first","affiliation":[]},{"given":"Hidenao","family":"Iwane","sequence":"additional","affiliation":[]},{"given":"Takuya","family":"Matsuzaki","sequence":"additional","affiliation":[]},{"given":"Hirokazu","family":"Anai","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,4,16]]},"reference":[{"key":"21_CR1","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, pp. 1\u20138. ACM (2014)","DOI":"10.1145\/2608628.2627488"},{"key":"21_CR2","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 2007, pp. 54\u201360. ACM, New York (2007)","DOI":"10.1145\/1277548.1277557"},{"issue":"3","key":"21_CR3","first-page":"27","volume":"2","author":"CC Chang","year":"2011","unstructured":"Chang, C.C., Lin, C.J.: LIBSVM: a library for support vector machines. ACM Trans. Intell. Syst. Technol. (TIST) 2(3), 27 (2011)","journal-title":"ACM Trans. Intell. Syst. Technol. (TIST)"},{"key":"21_CR4","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, pp. 111\u2013118. ACM (2004)","DOI":"10.1145\/1005285.1005303"},{"key":"21_CR5","unstructured":"Hsu, C.W., Chang, C.C., Lin, C.J., et al.: A practical guide to support vector classification (2003)"},{"key":"21_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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., England, M., Wilson, D., Davenport, J.H., Paulson, L.C., 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.) CICM 2014. LNCS, vol. 8543, pp. 92\u2013107. Springer, Heidelberg (2014)"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-319-02297-0_17","volume-title":"Computer Algebra in Scientific Computing","author":"H Iwane","year":"2013","unstructured":"Iwane, H., Higuchi, H., Anai, H.: An effective implementation of a special quantifier elimination for a sign definite condition by logical formula simplification. In: Gerdt, V.P., Koepf, W., Mayr, E.W., Vorozhtsov, E.V. (eds.) CASC 2013. LNCS, vol. 8136, pp. 194\u2013208. Springer, Heidelberg (2013)"},{"key":"21_CR8","unstructured":"Iwane, H., Matsuzaki, T., Arai, N., Anai, H.: Automated natural language geometry math problem solving by real quantifier elimination. In: Proceedings of the 10th International Workshop on Automated Deduction in Geometry, pp. 75\u201384 (2014)"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"518","DOI":"10.1007\/978-3-662-44199-2_78","volume-title":"Mathematical Software \u2013 ICMS 2014","author":"H Iwane","year":"2014","unstructured":"Iwane, H., Yanami, H., Anai, H.: SyNRAC: a toolbox for solving real algebraic constraints. In: Hong, H., Yap, C. (eds.) ICMS 2014. LNCS, vol. 8592, pp. 518\u2013522. Springer, Heidelberg (2014)"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Matsuzaki, T., Iwane, H., Anai, H., Arai, N.H.: The most uncreative examinee: a first step toward wide coverage natural language math problem solving. In: Twenty-Eighth AAAI Conference on Artificial Intelligence, pp. 1098\u20131104 (2014)","DOI":"10.1609\/aaai.v28i1.8869"},{"key":"21_CR11","unstructured":"Strzebo\u0144ski, A.W.: Real quantifier elimination for non-prenex formulas (2011). unpublished manuscript"}],"container-title":["Lecture Notes in Computer Science","Mathematical Aspects of Computer and Information Sciences"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-32859-1_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,17]],"date-time":"2023-08-17T17:24:01Z","timestamp":1692293041000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-32859-1_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319328584","9783319328591"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-32859-1_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}