| Autor: |
Yoshinobu Kawabe, Shivashish Jaishy, Nobuhiro Ito |
| Rok vydání: |
2016 |
| Předmět: |
|
| Zdroj: |
2016 4th Intl Conf on Applied Computing and Information Technology/3rd Intl Conf on Computational Science/Intelligence and Applied Informatics/1st Intl Conf on Big Data, Cloud Computing, Data Science & Engineering (ACIT-CSII-BCD). |
| DOI: |
10.1109/acit-csii-bcd.2016.064 |
| Popis: |
With the development of artificial intelligence technology over several decades, it is getting possible to find useful knowledge from an enormous amount of data. Also, it is getting possible to solve the difficult problems which cannot be solved by a human prover. Actually, a Japanese research project called "Todai Robot Project" tries to develop an intelligent robot that passes an entrance examination of the University of Tokyo. A case study was conducted to solve a prep school's practice test with an artificial intelligence technology called "Torobo-kun". It attracted great attention because of the good results. It is interesting to clarify the kind of an entrance exam problem which can be solved with a computer-assisted theorem proving tool. In this study, we conduct a case study to solve an entrance exam of a top university with an interactive theorem proving tool. Specifically, we employ Larch Prover (LP) which is a theorem proving tool based on equational theory and we solve a Kyushu University's entrance exam problem of mathematics. |
| Databáze: |
OpenAIRE |
| Externí odkaz: |
|
