| Project/Area Number |
08558023
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 展開研究 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | KYOTO UNIVERSITY |
|---|
Principal Investigator |
SATO Masahiko Kyoto Univ., Dept.of Information Science, Professor, 工学研究科, 教授 (20027387)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
OHTANI Takeshi Fujitsu Research Laboratories, Inc., Researcher, 研究員
TAKEUTI Izumi Kyoto Univ., Dept.of Information Science, Instructor, 工学研究科, 助手 (20264583)
SAWAMURA Hajime Niigata Univ., Dept.of Information Engineering, Associate Professor, 工学部, 助教授 (40282991)
KAMEYAMA Yukiyoshi Kyoto Univ., Dept.of Information Science, Associate Professor, 工学研究科, 助教授 (10195000)
TATSUTA Makoto Kyoto Univ., Dept.of Mathematics, Associate Professor, 理学研究科, 助教授 (80216994)
|
|---|
| Project Period (FY) |
1996 – 1997
|
| Project Status |
Completed (Fiscal Year 1997)
|
| Budget Amount *help |
¥6,100,000 (Direct Cost: ¥6,100,000)
Fiscal Year 1997: ¥2,000,000 (Direct Cost: ¥2,000,000)
Fiscal Year 1996: ¥4,100,000 (Direct Cost: ¥4,100,000)
|
|---|
| Keywords | Constructive Programming / Interactive Proof System / Intuitionistic Logic / Classical Logic / Modal Logic / 証明支援システム / グラフィカルユーザインターフェース / 証明エンジン |
|---|
| Research Abstract |
In this two-year research project, we designed and implemented a prototypical software system which assists constructive programming. We also evaluated the system by making programming examples using it. In 1996, (1) we implemented an interpreter of a functional programming langauge LAMBDA which is a basis for all the software systems in this profect, and (2) we implemented an interactive theorem proving system for an intuitionistic first-order predicate calculus. Based on these results, in 1997, (3) we implemented an interactive theorem proving system for various logical systems such as many variants of modal logics, and (4) we implemented a constructive programming system for a classical logic.
(2) : We implemented an interactive theorem proving system with a sophisticated graphical user interface based on X window system. A part of our implementation is written in the programming language JAVA,and our design aimed at distributed programming (distributed proving) by modules. (3) : We
… More
extended the system (2) so that the target logical system need not be an intuitionistic first-order logic. Our implementation includes many variants of modal logics such as T,S4, S5, B and so on. The system can be regarded as a system towards a proving strategy independent of specific logics. (4) : Extracting algorithmic contents from classical proofs is a quite recent topic in constructive programming. We designed and implemented two different ways, one uses the catch/throw mechanism, and the other uses the first-class continuation. We then extracted algorithms from classical proofs.
Using the systems in (2)-(4), we wrote many programming (proving) examples. It is generally observed that, when specification of a program is rigidly written, the specified program is synthesized quite smoothly. As a result, we have shown that constructive programming can be applicable to much wider targets than befor, and our systems can be a first step towards a constructive programming system in the real industry. Less
|
