{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T04:57:26Z","timestamp":1725857846569},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319402284"},{"type":"electronic","value":"9783319402291"}],"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-40229-1_15","type":"book-chapter","created":{"date-parts":[[2016,6,11]],"date-time":"2016-06-11T08:54:04Z","timestamp":1465635244000},"page":"213-227","source":"Crossref","is-referenced-by-count":3,"title":["Race Against the Teens \u2013 Benchmarking Mechanized Math on Pre-university Problems"],"prefix":"10.1007","author":[{"given":"Takuya","family":"Matsuzaki","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hidenao","family":"Iwane","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Munehiro","family":"Kobayashi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yiyang","family":"Zhan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ryoya","family":"Fukasaku","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jumma","family":"Kudo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hirokazu","family":"Anai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Noriko H.","family":"Arai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,12]]},"reference":[{"key":"15_CR1","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2010). www.SMT-LIB.org"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Bos, J.: Wide-coverage semantic analysis with boxer. In: Bos, J., Delmonte, R. (eds.) Semantics in Text Processing, STEP 2008 Conference Proceedings, pp. 277\u2013286. Research in Computational Semantics, College Publications (2008)","DOI":"10.3115\/1626481.1626503"},{"key":"15_CR3","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1162\/coli.2007.33.4.493","volume":"33","author":"S Clark","year":"2007","unstructured":"Clark, S., Curran, J.R.: Wide-coverage efficient statistical parsing with CCG and log-linear models. Comput. Linguist. 33, 493\u2013552 (2007)","journal-title":"Comput. Linguist."},{"key":"15_CR4","unstructured":"Dennis, L.A., Gow, J., Sch\u00fcrmann, C.: Challenge problems for inductive theorem provers v1.0. Technical report ULCS-07-004, University of Liverpool, Department of Computer Science (2007)"},{"issue":"2","key":"15_CR5","first-page":"153","volume":"3","author":"A Grabowski","year":"2010","unstructured":"Grabowski, A., Korni lowicz, A., Naumowicz, A.: Mizar in a nutshell. J. Formalized Reasoning 3(2), 153\u2013245 (2010)","journal-title":"J. Formalized Reasoning"},{"key":"15_CR6","unstructured":"Hoos, H.H., St\u00fctzle, T.: SATLIB: An Online Resource for Research on SAT. In: Sat2000: Highlights of Satisfiability Research in the Year 2000, pp. 283\u2013292. IOS Press, Amsterdam (2000)"},{"key":"15_CR7","unstructured":"Iwane, H., Matsuzaki, T., Arai, N., Anai, H.: Automated natural language geometry math problem solving by real quantier elimination. In: Proceedings of the 10th International Workshop on Automated Deduction (ADG2014), pp. 75\u201384 (2014)"},{"key":"15_CR8","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/j.tcs.2012.10.020","volume":"479","author":"H Iwane","year":"2013","unstructured":"Iwane, H., Yanami, H., Anai, H., Yokoyama, K.: An effective implementation of symbolic-numeric cylindrical algebraic decomposition for quantifier elimination. Theor. Comput. Sci. 479, 43\u201369 (2013)","journal-title":"Theor. Comput. Sci."},{"key":"15_CR9","unstructured":"Kwiatkowksi, T., Zettlemoyer, L., Goldwater, S., Steedman, M.: Inducing probabilistic CCG grammars from logical form with higher-order unification. In: Proceedings of the 2010 Conference on Empirical Methods in Natural Language Processing, pp. 1223\u20131233. Association for Computational Linguistics (2010)"},{"key":"15_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: Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, pp. 1098\u20131104 (2014)","DOI":"10.1609\/aaai.v28i1.8869"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/978-3-642-25070-5_10","volume-title":"Automated Deduction in Geometry","author":"P Quaresma","year":"2011","unstructured":"Quaresma, P.: Thousands of geometric problems for geometric theorem provers (TGTP). In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds.) ADG 2010. LNCS, vol. 6877, pp. 169\u2013181. Springer, Heidelberg (2011)"},{"issue":"4","key":"15_CR12","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure: the FOF and CNF Parts, v3.5.0. J. Autom. Reasoning 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reasoning"},{"issue":"1","key":"15_CR13","first-page":"1","volume":"3","author":"G Sutcliffe","year":"2010","unstructured":"Sutcliffe, G., Benzm\u00fcller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Formalized Reasoning 3(1), 1\u201327 (2010)","journal-title":"J. Formalized Reasoning"},{"key":"15_CR14","unstructured":"Sutcliffe, G., Stickel, M., Schulz, S., Urban, J.: Answer extraction for TPTP. http:\/\/www.cs.miami.edu\/~tptp\/TPTP\/Proposals\/AnswerExtraction.html"},{"key":"15_CR15","doi-asserted-by":"crossref","DOI":"10.1525\/9780520348097","volume-title":"A Decision Method for Elementary Algebra and Geometry","author":"A Tarski","year":"1951","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley (1951)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40229-1_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,1]],"date-time":"2022-07-01T11:40:57Z","timestamp":1656675657000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40229-1_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319402284","9783319402291"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40229-1_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}