| 研究課題/領域番号 |
02302009
|
|---|
| 研究種目 |
総合研究(A)
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
数学一般
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
佐藤 雅彦 東北大学, 電気通信研究所, 教授 (20027387)
|
|---|
| 研究分担者 |
亀山 幸義 東北大学, 電気通信研究所, 助手 (10195000)
龍田 真 東北大学, 電気通信研究所, 助手 (80216994)
|
|---|
| 研究期間 (年度) |
1990 – 1992
|
| 研究課題ステータス |
完了 (1992年度)
|
| 配分額 *注記 |
11,500千円 (直接経費: 11,500千円)
1992年度: 3,500千円 (直接経費: 3,500千円)
1991年度: 3,700千円 (直接経費: 3,700千円)
1990年度: 4,300千円 (直接経費: 4,300千円)
|
|---|
| キーワード | プログラム理論 / 構成的論理 / 型理論 / グラフ理論 / 直観主義論理 |
|---|
| 研究概要 |
(1)基礎数理、(2)応用数理、(3)プログラミングの3つの主題について、プログラミングの基礎となる理論の構築、理論に基づくプログラム開発方式の研究、実際の応用プログラムの開発を行った。プログラムの基礎的諸理論について考察し、相互の関連を検討するこにより、各理論を深化させることができた。特に、本研究により次のような研究成果を得た。
佐藤は、証明を内的対象としてもつ論理体系RPTを構成し、プログラム理論の基礎を与えた。龍田は、構成的プログラミングのための帰納的定義の実現可能性解釈について研究した。亀山は、構成的プログラミングシステムの作成および研究活動の基盤となる計算機ネットワークに関する研究を行った。伊藤は、並列プロセスの構造化モでルと項書換え計算モデルについて研究を行い、それらに基づくソフトウェアの試作をした。林は、Singleton,union,intersectionによる型理論の新しい枠組を提唱し、これが、constructive programmingのためには、従来の型理論の枠組より強力な表現力をもつことを示した。萩谷は、形式的な証明を記述するための計算機環境を構築するために必要と考えられる基礎的な技術、特に、例による証明、例を用いた証明、証明の視覚化等を含む証明チェッカのユーザ・インターフェースに関する研究を行った。小野は、構造規則を欠いた論理のセマンティクス、決定問題、有限モデル性について、いくつかの結果を得た。野下は、ゲーム木の高速探索技法を開発し,詰将棋を解くプログラムに応用した。牛島は、並行処理プログラムのテスト法およびデバッグ法の基礎と実際について研究した。
|
