| 研究課題/領域番号 |
08680356
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
小野 寛晰 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (90055319)
|
|---|
| 研究分担者 |
青戸 等人 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (00293390)
鹿島 亮 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (10240756)
石原 哉 北陸先端科学技術大学院大学, 情報科学研究科, 助教授 (10211046)
外山 芳人 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (00251968)
WOLTER Frank 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (20272990)
酒井 正彦 北陸先端科学技術大学院大学, 情報科学研究科, 助教授 (50215597)
|
|---|
| 研究期間 (年度) |
1996 – 1997
|
| 研究課題ステータス |
完了 (1997年度)
|
| 配分額 *注記 |
2,400千円 (直接経費: 2,400千円)
1997年度: 1,300千円 (直接経費: 1,300千円)
1996年度: 1,100千円 (直接経費: 1,100千円)
|
|---|
| キーワード | 部分構造論理 / 様相論理 / 項書換え系 / 構成的数学 / 時間論理 / 項書き換え系 |
|---|
| 研究概要 |
本研究の目標は、計算機科学に現われる数理論理学の問題を理論と応用の両面から解明しようとするものである。本年度に得られた成果のうちの主要なものを以下にあげる。
1.代数的手法による縮約のない部分構造論理の一般論の展開(小野)
2.部分構造論理におけるMaksimovaの変数分離の原理の研究(小野)
3.直感主義的様相論理の研究(青戸、小野)
4.項書き換え系における停止性および合流性に関する研究と関数型プログラム言語への応用(外山、青戸)
5.弱い含意命題論理に対する証明論(鹿島)
6.構成的数学の展開(石原)
1)の縮約規則をもたない論理の一般論については、小野はその成果をポーランド、スウェーデン、スペイン、ドイツで発表した。また北陸先端科学技術大学院大学において、オーストラリアのM.Bunder博士、R.Gore博士およびアメリカのA.Scedrov教授とそれぞれ部分構造論理に関する共同研究をおこなった。2)については、いくつかの部分構造論理に対しMaksimovaの原理を証明論的手法により証明した。このようなアプローチはこの研究が始めてである。3)の直観主義様相論理については、青戸がその有限モデル性についての興味深い結果を示した。4)の項書き換え系とその応用については、外山と青戸が精力的に研究をおこない、優れた成果をおさめている。弱い含意論理におけるcut elimination theoremについては鹿島が、また構成的数学については石原がいくつかの成果をあげた。
|
