{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T14:39:20Z","timestamp":1777559960753,"version":"3.51.4"},"reference-count":41,"publisher":"SAGE Publications","issue":"3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AIC"],"published-print":{"date-parts":[[2018,5,17]]},"DOI":"10.3233\/aic-180762","type":"journal-article","created":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T11:18:56Z","timestamp":1523618336000},"page":"251-266","source":"Crossref","is-referenced-by-count":4,"title":["Can an A.I. win a medal in the mathematical olympiad? \u2013 Benchmarking mechanized mathematics on pre-university problems1"],"prefix":"10.1177","volume":"31","author":[{"given":"Takuya","family":"Matsuzaki","sequence":"first","affiliation":[{"name":"Nagoya University, Japan. E-mail:\u00a0matuzaki@nuee.nagoya-u.ac.jp"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hidenao","family":"Iwane","sequence":"additional","affiliation":[{"name":"Fujitsu Laboratories, Ltd., Japan. E-mails:\u00a0iwane@jp.fujitsu.com,\u00a0anai@jp.fujitsu.com"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Munehiro","family":"Kobayashi","sequence":"additional","affiliation":[{"name":"University of Tsukuba, Japan. E-mail:\u00a0munehiro-k@math.tsukuba.ac.jp"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yiyang","family":"Zhan","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris Diderot, France. E-mail:\u00a0pon.zhan@gmail.com"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ryoya","family":"Fukasaku","sequence":"additional","affiliation":[{"name":"Tokyo University of Science, Japan. E-mails:\u00a0ryoya.0323@gmail.com,\u00a01414606@alumni.tus.ac.jp"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jumma","family":"Kudo","sequence":"additional","affiliation":[{"name":"Tokyo University of Science, Japan. E-mails:\u00a0ryoya.0323@gmail.com,\u00a01414606@alumni.tus.ac.jp"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hirokazu","family":"Anai","sequence":"additional","affiliation":[{"name":"Fujitsu Laboratories, Ltd., Japan. E-mails:\u00a0iwane@jp.fujitsu.com,\u00a0anai@jp.fujitsu.com"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Noriko H.","family":"Arai","sequence":"additional","affiliation":[{"name":"National Institute of Informatics, Japan. E-mail:\u00a0arai@nii.ac.jp"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","reference":[{"issue":"3","key":"10.3233\/AIC-180762_ref1","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10817-009-9149-2","article-title":"MetiTarski: An automatic theorem prover for real-valued special functions","volume":"44","author":"Akbarpour","year":"2010","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"10.3233\/AIC-180762_ref2","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/S0304-3975(96)80704-3","article-title":"Tractability of cut-free Gentzen type propositional calculus with permutation inference","volume":"170","author":"Arai","year":"1996","journal-title":"Theoretical Computer Science"},{"key":"10.3233\/AIC-180762_ref3","unstructured":"N.H.\u00a0Arai and R.\u00a0Masukawa, How to find symmetries hidden in combinatorial problems, in: Proceedings of the Eighth Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, 2000."},{"key":"10.3233\/AIC-180762_ref4","doi-asserted-by":"crossref","unstructured":"R.\u00a0Atkey, P.\u00a0Johann and A.\u00a0Kennedy, Abstraction and invariance for algebraically indexed types, in: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL \u201913, ACM, New York, NY, USA, 2013, pp.\u00a087\u2013100, http:\/\/doi.acm.org\/10.1145\/2429069.2429082.","DOI":"10.1145\/2429069.2429082"},{"issue":"3","key":"10.3233\/AIC-180762_ref5","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/s10817-015-9356-y","article-title":"A heuristic prover for real inequalities","volume":"56","author":"Avigad","year":"2016","journal-title":"Journal of Automated Reasoning"},{"key":"10.3233\/AIC-180762_ref8","doi-asserted-by":"publisher","DOI":"10.3115\/1626481.1626503"},{"key":"10.3233\/AIC-180762_ref9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jsc.2015.11.002","article-title":"Truth table invariant cylindrical algebraic decomposition","volume":"76","author":"Bradford","year":"2016","journal-title":"Journal of Symbolic Computation"},{"key":"10.3233\/AIC-180762_ref10","doi-asserted-by":"publisher","DOI":"10.1145\/2755996.2756654"},{"issue":"C","key":"10.3233\/AIC-180762_ref11","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1016\/j.jsc.2015.11.008","article-title":"Quantifier elimination by cylindrical algebraic decomposition based on regular chains","volume":"75","author":"Chen","year":"2016","journal-title":"Journal of Symbolic Computation"},{"key":"10.3233\/AIC-180762_ref12","doi-asserted-by":"publisher","DOI":"10.1162\/coli.2007.33.4.493"},{"issue":"1\u20132","key":"10.3233\/AIC-180762_ref13","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S0747-7171(88)80004-X","article-title":"Real quantifier elimination is doubly exponential","volume":"5","author":"Davenport","year":"1988","journal-title":"Journal of Symbolic Computation"},{"key":"10.3233\/AIC-180762_ref15","unstructured":"M.\u00a0England and J.H.\u00a0Davenport, Experience with heuristics, benchmarks & standards for cylindrical algebraic decomposition, in: Proceedings of the 1st Workshop on Satisfiability Checking and Symbolic Computation Co-Located with 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2016), Timisoara, Romania, September 24, 2016, E.\u00a0\u00c1brah\u00e1m, J.H.\u00a0Davenport and P.\u00a0Fontaine, eds, CEUR Workshop Proceedings, Vol.\u00a01804, CEUR-WS.org, 2016, pp.\u00a024\u201331, http:\/\/ceur-ws.org\/Vol-1804\/paper-06.pdf."},{"key":"10.3233\/AIC-180762_ref16","doi-asserted-by":"crossref","unstructured":"R.\u00a0Fukasaku, H.\u00a0Iwane and Y.\u00a0Sato, Improving a CGS-QE algorithm, in: Revised Selected Papers of the 6th International Conference on Mathematical Aspects of Computer and Information Sciences \u2013 Volume 9582. MACIS 2015, Springer-Verlag Inc., New York, NY, USA, 2016, pp.\u00a0231\u2013235.","DOI":"10.1007\/978-3-319-32859-1_20"},{"key":"10.3233\/AIC-180762_ref17","unstructured":"J.P.\u00a0Gelb, Experiments with a natural language problem-solving system, in: Proceedings of the 2nd International Joint Conference on Artificial Intelligence. IJCAI\u201971, Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 1971, pp.\u00a0455\u2013462."},{"issue":"2","key":"10.3233\/AIC-180762_ref18","first-page":"153","article-title":"Mizar in a nutshell","volume":"3","author":"Grabowski","year":"2010","journal-title":"Journal of Formalized Reasoning"},{"key":"10.3233\/AIC-180762_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_3"},{"key":"10.3233\/AIC-180762_ref20","first-page":"283","volume-title":"SATLIB: An Online Resource for Research on SAT","author":"Hoos","year":"2000"},{"key":"10.3233\/AIC-180762_ref21","doi-asserted-by":"publisher","DOI":"10.3115\/v1\/D14-1058"},{"key":"10.3233\/AIC-180762_ref22","doi-asserted-by":"crossref","unstructured":"H.\u00a0Iwane and H.\u00a0Anai, Formula simplification for real quantifier elimination using geometric invariance, in: Proceedings of the 42nd International Symposium on Symbolic and Algebraic Computation (ISSAC-2017), 2017, to appear.","DOI":"10.1145\/3087604.3087627"},{"key":"10.3233\/AIC-180762_ref23","unstructured":"H.\u00a0Iwane, T.\u00a0Matsuzaki, N.\u00a0Arai and H.\u00a0Anai, Automated natural language geometry math problem solving by real quantier elimination, in: Proceedings of the 10th International Workshop on Automated Deduction (ADG2014), 2014, pp.\u00a075\u201384."},{"key":"10.3233\/AIC-180762_ref24","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/j.tcs.2012.10.020","article-title":"An effective implementation of symbolic-numeric cylindrical algebraic decomposition for quantifier elimination","volume":"479","author":"Iwane","year":"2013","journal-title":"Theor. Comput. Sci."},{"key":"10.3233\/AIC-180762_ref25","unstructured":"C.\u00a0Kaliszyk, G.\u00a0Sutcliffe and F.\u00a0Rabe, TH1: The TPTP typed higher-order form with rank-1 polymorphism, in: Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning (PAAR 2016), 2016, pp.\u00a041\u201355."},{"key":"10.3233\/AIC-180762_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/11618027_6"},{"key":"10.3233\/AIC-180762_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-32859-1_21"},{"key":"10.3233\/AIC-180762_ref28","doi-asserted-by":"crossref","first-page":"585","DOI":"10.1162\/tacl_a_00160","article-title":"Parsing algebraic word problems into equations","volume":"3","author":"Koncel-Kedziorski","year":"2015","journal-title":"Transactions of the Association for Computational Linguistics"},{"key":"10.3233\/AIC-180762_ref29","doi-asserted-by":"publisher","DOI":"10.3115\/v1\/P14-1026"},{"key":"10.3233\/AIC-180762_ref30","unstructured":"T.\u00a0Kwiatkowksi, L.\u00a0Zettlemoyer, S.\u00a0Goldwater and M.\u00a0Steedman, Inducing probabilistic CCG grammars from logical form with higher-order unification, in: Proceedings of the 2010 Conference on Empirical Methods in Natural Language Processing, Association for Computational Linguistics, 2010, pp.\u00a01223\u20131233."},{"key":"10.3233\/AIC-180762_ref31","doi-asserted-by":"crossref","unstructured":"T.\u00a0Matsuzaki, T.\u00a0Ito, H.\u00a0Iwane, H.\u00a0Anai and N.H.\u00a0Arai, Semantic parsing of pre-university math problems, in: Proceedings of the 55th Annual Meeting of the Association for Computational Linguistics. Association for Computational Linguistics, 2017, to appear.","DOI":"10.18653\/v1\/P17-1195"},{"key":"10.3233\/AIC-180762_ref32","doi-asserted-by":"crossref","unstructured":"T.\u00a0Matsuzaki, H.\u00a0Iwane, H.\u00a0Anai and N.H.\u00a0Arai, 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, 2014, pp.\u00a01098\u20131104.","DOI":"10.1609\/aaai.v28i1.8869"},{"key":"10.3233\/AIC-180762_ref33","doi-asserted-by":"crossref","unstructured":"T.\u00a0Matsuzaki, H.\u00a0Iwane, M.\u00a0Kobayashi, Y.\u00a0Zhan, R.\u00a0Fukasaku, J.\u00a0Kudo, H.\u00a0Anai and N.H.\u00a0Arai, Race against the teens \u2013 benchmarking mechanized math on pre-university problems, in: Automated Reasoning \u2013 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27, N.\u00a0Olivetti and A.\u00a0Tiwari, eds, Proceedings. Lecture Notes in Computer Science, Vol.\u00a09706, Springer, 2016, pp.\u00a0213\u2013227, July 2, 2016.","DOI":"10.1007\/978-3-319-40229-1_15"},{"key":"10.3233\/AIC-180762_ref34","unstructured":"T.\u00a0Matsuzaki, M.\u00a0Kobayashi and N.H.\u00a0Arai, An information-processing account of representation change: International mathematical olympiad problems are hard not only for humans, in: Proceedings of the 38th Annual Conference of the Cognitive Science Society, Cognitive Science Society, 2016, pp.\u00a02297\u20132302."},{"key":"10.3233\/AIC-180762_ref36","doi-asserted-by":"crossref","unstructured":"A.\u00a0Mitra and C.\u00a0Baral, Learning to use formulas to solve simple arithmetic problems, in: Proceedings of the 54th Annual Meeting of the Association for Computational Linguistics, 2016, pp.\u00a02144\u20132153.","DOI":"10.18653\/v1\/P16-1202"},{"key":"10.3233\/AIC-180762_ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25070-5_10"},{"issue":"4","key":"10.3233\/AIC-180762_ref38","first-page":"429","article-title":"Automating change of representation for proofs in","volume":"10","author":"Raggi","year":"2016","journal-title":"Discrete Mathematics (Extended Version). Mathematics in Computer Science"},{"key":"10.3233\/AIC-180762_ref39","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/D15-1202"},{"key":"10.3233\/AIC-180762_ref40","doi-asserted-by":"crossref","unstructured":"S.\u00a0Shi, Y.\u00a0Wang, C.-Y.\u00a0Lin, X.\u00a0Liu and Y.\u00a0Rui, Automatically solving number word problems by semantic parsing and reasoning, in: EMNLP, L.\u00a0M\u00e0rquez, C.\u00a0Callison-Burch, J.\u00a0Su, D.\u00a0Pighin and Y.\u00a0Marton, eds, The Association for Computational Linguistics, 2015, pp.\u00a01132\u20131142, http:\/\/dblp.uni-trier.de\/db\/conf\/emnlp\/emnlp2015.html#ShiWLLR15.","DOI":"10.18653\/v1\/D15-1135"},{"key":"10.3233\/AIC-180762_ref42","doi-asserted-by":"crossref","unstructured":"M.\u00a0Steedman, The Syntactic Process. Bradford Books, MIT Press, Cambridge, 2001.","DOI":"10.7551\/mitpress\/6591.001.0001"},{"issue":"C","key":"10.3233\/AIC-180762_ref43","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1016\/j.jsc.2015.11.018","article-title":"Cylindrical algebraic decomposition using local projections","volume":"76","author":"Strzebo\u0144ski","year":"2016","journal-title":"Journal of Symbolic Computation"},{"issue":"4","key":"10.3233\/AIC-180762_ref44","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","article-title":"The TPTP problem library and associated infrastructure: The FOF and CNF parts, v3.5.0","volume":"43","author":"Sutcliffe","year":"2009","journal-title":"Journal of Automated Reasoning"},{"key":"10.3233\/AIC-180762_ref46","doi-asserted-by":"crossref","unstructured":"A.\u00a0Tarski, A Decision Method for Elementary Algebra and Geometry, University of California Press, Berkeley, 1951.","DOI":"10.1525\/9780520348097"},{"key":"10.3233\/AIC-180762_ref47","doi-asserted-by":"crossref","unstructured":"L.\u00a0Zhou, S.\u00a0Dai and L.\u00a0Chen, Learn to solve algebra word problems using quadratic programming, in: EMNLP, L.\u00a0M\u00e0rquez, C.\u00a0Callison-Burch, J.\u00a0Su, D.\u00a0Pighin and Y.\u00a0Marton, eds, The Association for Computational Linguistics, 2015, pp.\u00a0817\u2013822, http:\/\/dblp.uni-trier.de\/db\/conf\/emnlp\/emnlp2015.html#ZhouDC15.","DOI":"10.18653\/v1\/D15-1096"}],"container-title":["AI Communications"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/AIC-180762","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T18:27:47Z","timestamp":1777400867000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/AIC-180762"}},"subtitle":[],"editor":[{"given":"Pascal","family":"Fontaine","sequence":"additional","affiliation":[],"role":[{"role":"editor","vocabulary":"crossref"}]},{"given":"Cezary","family":"Kaliszyk","sequence":"additional","affiliation":[],"role":[{"role":"editor","vocabulary":"crossref"}]},{"given":"Stephan","family":"Schulz","sequence":"additional","affiliation":[],"role":[{"role":"editor","vocabulary":"crossref"}]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[],"role":[{"role":"editor","vocabulary":"crossref"}]}],"short-title":[],"issued":{"date-parts":[[2018,5,17]]},"references-count":41,"journal-issue":{"issue":"3"},"URL":"https:\/\/doi.org\/10.3233\/aic-180762","relation":{},"ISSN":["1875-8452","0921-7126"],"issn-type":[{"value":"1875-8452","type":"electronic"},{"value":"0921-7126","type":"print"}],"subject":[],"published":{"date-parts":[[2018,5,17]]}}}