| Project/Area Number |
11680359
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | KOBE UNIVERSITY |
|---|
Principal Investigator |
TAKAHASHI Makoto (2000) Kobe University, Faculty of Human Development, Associate Professor, 発達科学部, 助教授 (50154860)
田村 直之 (1999) 神戸大学, 工学部, 助教授 (60207248)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
BANBARA Mutsunori NARA National College of Technology, Department of Liberal Studies, Lecturer, 一般教科, 講師 (80290774)
TAMURA Naoyuki Kobe University, Faculty of Engineering, Associate Professor, 工学部, 助教授 (60207248)
高橋 真 神戸大学, 発達科学部, 助教授 (50154860)
|
|---|
| Project Period (FY) |
1999 – 2000
|
| Project Status |
Completed (Fiscal Year 2000)
|
| Budget Amount *help |
¥3,100,000 (Direct Cost: ¥3,100,000)
Fiscal Year 2000: ¥1,300,000 (Direct Cost: ¥1,300,000)
Fiscal Year 1999: ¥1,800,000 (Direct Cost: ¥1,800,000)
|
|---|
| Keywords | Temporal Linear Logic / Linear Logic / Temporal Logic / Logic Programming Language / Intuitionism / Compiler / 時相腺形論理 |
|---|
| Research Abstract |
In this research project, the followings are accomplished : the design of Intuitionistic Temporal Linear Logic system ITLL, the design of a logic programming language TLLP which is based on ITLL, and the development of the compiler system of TLLP.
In addition to linear logic operators, ITLL has the following logical operators : a modal operator ○ which is used to specify a resource usable only once at the next time, a modal operator □ which is used to specify a resource usable only once at any time, and a modal operator ! which is used to specify a resource usable any number of times and at any time. All of intuitionistic logic, intuitionistic linear logic, and intuitionistic temporal logic can be embedded into ITLL.
Logic programming language TLLP is based on this ITLL, and it is a super-set of Prolog and a linear logic programming language LLP.In TLLP, it is possible to represent a concept of time-dependent resource consumption.
Computation model of TLLP is given by extending the idea of Miller's uniform proof, Hodas's IO-model, and leveled IO-model of LLP.
Compiler of TLLP is based on the extended leveled IO-model which enables the efficient execution of TLLP programs.
In order to investigate a further efficient implementation of TLLP, we also studied about a translator system of a linear logic programming language into Java and about a static analysis method of a classical linear logic programming language.
|
