| 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)
|
|---|
| Project Period (FY) |
1988 – 1990
|
| Keywords | Program Synthesis / Theorem Proving / Non-classical Logic / Cellular Automata / Graph Algorithms / Distributed Operating System / Constructive Mathematics |
|---|
| 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.
|
