Project/Area Number  10480063 
Research Category 
GrantinAid for Scientific Research (B).

Section  一般 
Research Field 
計算機科学

Research Institution  Kobe University 
Principal Investigator 
HAYASHI Susumu Kobe University, Department of Computer and Systems Engineering, Professor, 工学部, 教授 (40156443)

CoInvestigator(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 Fiscal Year 
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 / 形式的証明の開発 / 定理証明 / 論理情報の視覚化 / 古典論理証明の実行 / CurryHowardの対応 / 学習理論 
Research Abstract 
Some theories of classical proof exectution were examined if they are good for proof animation. We implemented an environment for PA by Ogatatheory 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.
