| 研究課題/領域番号 |
08680356
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
小野 寛晰 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (90055319)
|
|---|
| 研究分担者 |
青戸 等人 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (00293390)
鹿島 亮 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (10240756)
石原 哉 北陸先端科学技術大学院大学, 情報科学研究科, 助教授 (10211046)
外山 芳人 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (00251968)
|
|---|
| キーワード | 部分構造論理 / 様相論理 / 項書換え系 / 構成的数学 |
|---|
| 研究概要 |
本研究の目標は、計算機科学に現われる数理論理学の問題を理論と応用の両面から解明しようとするものである。本年度に得られた成果のうちの主要なものを以下にあげる。
1.代数的手法による縮約のない部分構造論理の一般論の展開(小野)
2.部分構造論理におけるMaksimovaの変数分離の原理の研究(小野)
3.直観主義的様相論理の研究(青戸、小野)
4.項書き換え系における停止性および合流性に関する研究と関数型プログラム言語への応用(外山、青戸)
5.弱い含意命題論理に対する証明論(鹿島)
6.構成的数学の展開(石原)
1)の縮約規則をもたない論理の一般論については、小野はその成果をポーランド、スウェーデン、スペイン、ドイツで発表した。2)については、いくつかの部分構造論理に対しMaksimovaの原理を証明論的手法により証明した。このようなアプローチはこの研究が初めてである。3)の直観主義様相論理については、青戸がその有限モデル性についての興味深い結果を示した。4)の項書き換え系とその応用については、外山と青戸が精力的に研究をおこない、優れた成果をおさめている。弱い含意論理における。cut elimination theoremについては鹿島が、また構成的数学については石原がいくつかの成果をあげた。
|
