| Project/Area Number |
10480063
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B).
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Kobe University |
|---|
Principal Investigator |
HAYASHI Susumu Kobe University, Department of Computer and Systems Engineering, Professor, 工学部, 教授 (40156443)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
SATO Masahiko Kyoto University, Graduate School, Department of Computer Science, Professor, 大学院・工学研究科, 教授 (20027387)
YASUGI Mariko Kyoto Sangyo University, Department of Computer Science, Professor, 理学部, 教授 (90022277)
TAMURA Naoyuki Kobe University, Department of Computer and Systems Engineering, Associate Professor, 工学部, 助教授 (60207248)
|
|---|
| Project Period (FY) |
1998 – 2000
|
| Project Status |
Completed (Fiscal Year 2000)
|
| Budget Amount *help |
¥6,300,000 (Direct Cost: ¥6,300,000)
Fiscal Year 2000: ¥1,300,000 (Direct Cost: ¥1,300,000)
Fiscal Year 1999: ¥1,500,000 (Direct Cost: ¥1,500,000)
Fiscal Year 1998: ¥3,500,000 (Direct Cost: ¥3,500,000)
|
|---|
| Keywords | constructive programming / program verification / program logic / learning theory / classical proof execution / 学習理論 |
|---|
| Research Abstract |
Some theories of classical proof exectution were examined if they are good for proof animation. We implemented an environment for PA by Ogata-theory and it was tested on simple examles. Berardi theory was also deeply examined theoretically and practically by a computer experiment. It turned out that existing theory are short for the aim.
To break through the limitation of the existing theories, we developed a new theory of classical proof execution. It is based on the ideas from algorithmic learning theory and is entirely different from the existing theories. The theory is called LCM(Limit Computable Mathematics).
Application of LCM to PA was investigated. Maybe, even more importantly, it turned out that LCM has a lot of deep connections to various theories in computer science and logic. Examples are computation on real numbers, basis theorems in recursion theory, reverse mathematics of principles of classical logic, concurrent computation, computer algebra of invariant theory, etc. etc.. This idea stimulated many researchers and some projects independent from and/or collaborated with us are taking place.
|
