1997 Fiscal Year Annual Research Report
| Project/Area Number |
08680356
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology, Hokuriku |
|---|
Principal Investigator |
小野 寛晰 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (90055319)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
青戸 等人 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (00293390)
鹿島 亮 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (10240756)
石原 哉 北陸先端科学技術大学院大学, 情報科学研究科, 助教授 (10211046)
外山 芳人 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (00251968)
|
|---|
| Keywords | 部分構造論理 / 様相論理 / 項書換え系 / 構成的数学 |
|---|
| Research Abstract |
本研究の目標は、計算機科学に現われる数理論理学の問題を理論と応用の両面から解明しようとするものである。本年度に得られた成果のうちの主要なものを以下にあげる。
1.代数的手法による縮約のない部分構造論理の一般論の展開(小野)
2.部分構造論理におけるMaksimovaの変数分離の原理の研究(小野)
3.直観主義的様相論理の研究(青戸、小野)
4.項書き換え系における停止性および合流性に関する研究と関数型プログラム言語への応用(外山、青戸)
5.弱い含意命題論理に対する証明論(鹿島)
6.構成的数学の展開(石原)
1)の縮約規則をもたない論理の一般論については、小野はその成果をポーランド、スウェーデン、スペイン、ドイツで発表した。2)については、いくつかの部分構造論理に対しMaksimovaの原理を証明論的手法により証明した。このようなアプローチはこの研究が初めてである。3)の直観主義様相論理については、青戸がその有限モデル性についての興味深い結果を示した。4)の項書き換え系とその応用については、外山と青戸が精力的に研究をおこない、優れた成果をおさめている。弱い含意論理における。cut elimination theoremについては鹿島が、また構成的数学については石原がいくつかの成果をあげた。
|
-
[Publications] 小野寛晰: "Decidability and finite model property of substructural logics" Tbilisi Symposium on Language,Logic and Computation. (1998)
-
[Publications] 成瀬博之: "A syntactic approach to Maksimova's principle of variable separation for some substructural logics" Notre Dame Journal of Formal Logic. (発表予定).
-
[Publications] 青戸等人: "Persistency of confluence" Journal of Universal Computer Science. 3・11. 1134-1147 (1997)
-
[Publications] 青戸等人: "On composable properties of term rewriting systems" Lecture Nates in Computer Science. 1298. 114-128 (1997)
-
[Publications] 鹿島亮: "Contraction-elimination for implicational logics" Annals of Pure and Applied Logic. 84・1. 17-39 (1997)
