An Automated Deduction and Its Implementation for Solving Problem of Sequence at University Entrance Examination

摘要

"Todai Robot Project" is a project of artificial intelligence launched by National Institute of Informatics for re-unifying the artificial intelligence field subdivided in 1980s and afterwards. We focus towards attaining a high score in National Center Test for University Admissions, and use Quantifier Elimination (QE) over the real closed fields as a main tool for solving problems in mathematics. However, it is not applicable for several kinds of problems such as one with sequence. In this article, we propose an algorithm for solving problems of sequence at the National Center Test for University Admissions.