| Project/Area Number |
63302007
|
|---|
| Research Category |
Grant-in-Aid for Co-operative Research (A)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
General mathematics (including Probability theory/Statistical mathematics)
|
|---|
| Research Institution | Waseda University |
|---|
Principal Investigator |
HIROSE Ken Waseda University, Mathematics, Professor, 理工学部, 教授 (60063632)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
UESU Tadahiro Science Univ. of Tokyo, Mathematics, Professor, 理学部, 教授 (60015550)
YONEDA Nobuo Tokyo Denki Univ, Mathematical Science, Professor, 理工学部, 教授 (50080487)
NAKAJIMA Reiji Kyoto University, RIMS, Professor, 数理解析研究所, 教授 (60109080)
FUJINO Seiichi Kyushu University, Mathematics, Professor, 理学部, 教授 (20037146)
IRI Masao University of Tokyo, Applied Physics, Professor, 工学部, 教授 (40010722)
河原 康雄 九州大学, 理学部, 助教授 (90091181)
小野 寛晰 広島大学, 総合科学部, 教授 (90055319)
佐藤 雅彦 東北大学, 電気通信研究所, 教授 (20027387)
榎本 彦衛 東京大学, 理学部, 助教授 (00011669)
|
|---|
| Project Period (FY) |
1988 – 1990
|
| Project Status |
Completed (Fiscal Year 1990)
|
| Budget Amount *help |
¥10,500,000 (Direct Cost: ¥10,500,000)
Fiscal Year 1990: ¥3,000,000 (Direct Cost: ¥3,000,000)
Fiscal Year 1989: ¥3,600,000 (Direct Cost: ¥3,600,000)
Fiscal Year 1988: ¥3,900,000 (Direct Cost: ¥3,900,000)
|
|---|
| Keywords | Program Synthesis / Theorem Proving / Non-classical Logic / Cellular Automata / Graph Algorithms / Distributed Operating System / Constructive Mathematics / 算譜の仕様 / 算譜の検証 / 高階論理体系 / 分散OS / 算譜言語 / 算譜言語のモデル / 論理体系 / 幾何学算法 |
|---|
| Research Abstract |
More than twenty researchers worked in cooperation on four major fields, namely, (1) fundamental theories and automata, (2) discrete algorithms, (3) programming languages and program synthesis, and (4) theories on compilers and operating systems. Four local groups were organized : (a) Tokyo and Sendai, (b) Tsukuba, (c) Kyoto and Nagoya, and (d) Kyushu and Hiroshima. Research meetings were held by each groups and research conferences by the whole members were held to report and discuss results of the year at RIMS of Kyoto University every December.
Activities of the groups are as follows :
(a) Tokyo and Sendai Group K. Hirose. et al. proposed and implemented a new idea for theorem proving which utilizes various mathematical structures behind the targeted theories as meta-knowledge, and showed good results in time and space behavior of the prover. M. Sato. et al. investigated program synthesis as a constructive mathematics and proposed a hierarchical logic system to include provability' as a predicate in the system. T. Uesu. studied on axiomatization of theories. M. Iri. and H. Enomoto. et al. developed various discrete algorithms mainly in graphs and networks. M. Mori et al. developed algorithms and a system to display results of numerical computation in graphics.
(b) Tsukuba Group S. Igarashi. et al. introduces nu-conversion into program logics to handle real time constraints and concurrent processes. T. Nishimura et al. investigated machine handling of proof heuristics, especially for set theoretical theorems.
(c) Kyoto and Nagoya Group R. Nakajima et al. proposed and implemented a new discipline on distributed operating systems. T. Ohshiba et al. studied on proof procedures and proved Herbrand's theorem constructively.
(d) Kyushu and Hiroshima Group S. Fujino studied on formal languages and automata, especially on cellular automata and proved various properties of them. H. Ono studied on non-classical logics and their application to program synthesis and verification.
|
