1996 Fiscal Year Annual Research Report

理論計算機科学における数理論理学の応用

Research Project

Project/Area Number	08680356
Research Category	Grant-in-Aid for Scientific Research (C)
Research Institution	Japan Advanced Institute of Science and Technology
Principal Investigator	小野寛晰北陸先端科学技術大学院大学, 情報科学研究科, 教授 (90055319)
Co-Investigator(Kenkyū-buntansha)	WOLTER Frank 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (20272990) 鹿島亮北陸先端科学技術大学院大学, 情報科学研究科, 助手 (10240756) 酒井正彦北陸先端科学技術大学院大学, 情報科学研究科, 助教授 (50215597) 石原哉北陸先端科学技術大学院大学, 情報科学研究科, 助教授 (10211046) 外山芳人北陸先端科学技術大学院大学, 情報科学研究科, 教授 (00251968)
Keywords	部分構造論理 / 様相論理 / 時間論理 / 項書き換え系
Research Abstract	本研究の目標は、計算機科学に現われる数理論理学の問題を理論と応用の両面から解明しようとするものである。今年度において得られた成果のうちの主要なものを以下にあげる。 1.部分構造論理、とくに縮約のない論理の一般論への試み 2.様相論理および時間論理の研究の展開、とくに直観主義的様相論理の研究 3.弱い含意命題論理と型つきラムダ計算の関係の究明 4.項書き換え系における停止性および合流性に関する研究部分構造論理に関する研究はこれまで特定の論理の性質を調べることが中心であったが、小野は縮約のない論理について代数的手法により一般論を展開することを試みている。また、様相論理と時間論理についてはヴォルターが非常に精力的に研究をおこない、決定問題などにおいて著しい結果をあげた。また、外山と酒井はさまざまな項書き換え系における停止性および合流性についての優れた結果を得た。これらの研究を推進するために、国内の研究者との研究連絡、来日したポーランドの論理学者であるマリノフスキ教授との共同研究、本学に滞在中の様相論理に関する著名な研究者であるザハリャ-シチェフ客員助教授との共同研究を行ない、非常に実りある研究成果を得ることができた。これらの成果の一部は、千葉で行なわれた国際会議Logics for Linguistics,Philosophy and Cognitive Scienceにおいて、小野およびヴォルターにより招待講演の形で発表された。

Research Products
(9 results)

All Other

All Publications (9 results)

[Publications] 小野寛晰: "Decidability and the finite model property of substructural logics" The Tbilisi Symposium on Language,Logic and Computation. (1997)
[Publications] 小野寛晰: "Algebraic semantics for predicate logics and their completeness" Logic at Work. (1997)
[Publications] バュステルソ: "Cut-elimination in noncommutative substructural logics" Reports on Mathematical Logic. 30. (1997)
[Publications] 酒井正彦: "Semantics and strong sequentiality of priority term rewriting systems" Lecture Notes in Computer Sciene. 1103. 377-391 (1996)
[Publications] 高橋宜孝: "条件付き項書換え系の合流性について" 電子情報通信学会論文誌. J79-D-I. 877-902 (1996)
[Publications] ヴォルターフランク: "Tense logic without tense operators" Mathematical Logic Quarterly. 145-171 (1996)
[Publications] ヴォルターフランク: "Completeness and decidability of tense logics closely related to logics above K4" Journal of Symbolic Logic. (1996)
[Publications] ヴォルターフランク: "Properties of tense logics" Mathematical Logic Quarterly. (1996)
[Publications] 田中一之: "数学基礎論講義-不完全性定理とその発展" 日本評論社, 206 (1997)

1996 Fiscal Year Annual Research Report

理論計算機科学における数理論理学の応用

Principal Investigator

小野 寛晰 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (90055319)

Research Products

[Publications] 小野寛晰: "Decidability and the finite model property of substructural logics" The Tbilisi Symposium on Language,Logic and Computation. (1997)

[Publications] 小野寛晰: "Algebraic semantics for predicate logics and their completeness" Logic at Work. (1997)

[Publications] バュ ステルソ: "Cut-elimination in noncommutative substructural logics" Reports on Mathematical Logic. 30. (1997)

[Publications] 酒井正彦: "Semantics and strong sequentiality of priority term rewriting systems" Lecture Notes in Computer Sciene. 1103. 377-391 (1996)

[Publications] 高橋宜孝: "条件付き項書換え系の合流性について" 電子情報通信学会論文誌. J79-D-I. 877-902 (1996)

[Publications] ヴォルターフランク: "Tense logic without tense operators" Mathematical Logic Quarterly. 145-171 (1996)

[Publications] ヴォルターフランク: "Completeness and decidability of tense logics closely related to logics above K4" Journal of Symbolic Logic. (1996)

[Publications] ヴォルターフランク: "Properties of tense logics" Mathematical Logic Quarterly. (1996)

[Publications] 田中一之: "数学基礎論講義-不完全性定理とその発展" 日本評論社, 206 (1997)

小野寛晰北陸先端科学技術大学院大学, 情報科学研究科, 教授 (90055319)

[Publications] バュステルソ: "Cut-elimination in noncommutative substructural logics" Reports on Mathematical Logic. 30. (1997)