| Project/Area Number |
05302011
|
|---|
| 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 | Chiba University (1995)
University of Tsukuba (1993-1994) |
|---|
Principal Investigator |
TSUJI Takashi Chiba Univ., Science Prof., 理学部, 教授 (70016666)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
HITOTUMATU Shin Tokyo Elec.Univ., Eng. Prof., 理工学部, 教授 (10027378)
ONO Hiroakira JAIST Hokuriku, Inf.Sci. Prof., 情報科学研究科, 教授 (90055319)
NANBA Kanji Univ.of Tokyo, Math.Sci. Prof., 大学院数理科学研究科, 教授 (40015524)
YONEDA Nobuo Tokyo Elec.Univ., Eng. Prof., 理工学部, 教授 (50080487)
IGARASHI Shigeru Univ.of Tsukuba, Inf.Sci. Prof., 電子情報工学系, 教授 (80027367)
水谷 哲也 筑波大学, 電子・情報工学系, 講師 (70209758)
細野 千春 筑波大学, 電子・情報工学系, 助教授 (20108294)
|
|---|
| Project Period (FY) |
1993 – 1995
|
| Project Status |
Completed (Fiscal Year 1995)
|
| Budget Amount *help |
¥11,200,000 (Direct Cost: ¥11,200,000)
Fiscal Year 1995: ¥2,600,000 (Direct Cost: ¥2,600,000)
Fiscal Year 1994: ¥4,200,000 (Direct Cost: ¥4,200,000)
Fiscal Year 1993: ¥4,400,000 (Direct Cost: ¥4,400,000)
|
|---|
| Keywords | NU / logic / theory of programs / programming / graph theory / artificial inteligence / music information processing / ν-転換 / 時制算術 / プログラム検証 / 人工知能 |
|---|
| Research Abstract |
Owing to each of research fellows, good research results are established on subjects of this research project. Some of them are listed in the following.
1.Logic : a formal derivation of the decidability of the theory SA,extending intuitionistic linear logic, the finite model property for BCK and BCIW,algebraic semantics for predicate logic, decidability and finite model property of substructural logics, a new formalization of Feferman's system, natural proofs in automated proving, validity verification of knowledge predicats.
2.Theory of programs : locomorphism analytical equivalence theory, analysis of a real time problem in a software/hardware system in two ways using nu-conversion and by tense arithmetic, literal dependence net in concurrent logic programming environment, a typed lambda-calculus of proving-by-example, a transformation method for dynamic-sized tabulation, programming by example.
3.Programming : biding time analysis for data type specialization, programming techniques for effective use of pipe-line and cache, efficiency of computing determinants by a fraction-free processor.
4.Graph theory : graph decomposition with prescribed vertices, twist number of complete bipartite praphs.
5.Artificial inteligence : a mathematical theory of machine discovery from facs, formalization of planar graphs, analysis methods and tools of expression in music performances.
|
