2017 Fiscal Year Annual Research Report
Classical logic and infinite phenomena in computation
| Project/Area Number |
15K00012
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
中澤 巧爾 名古屋大学, 情報学研究科, 准教授 (80362581)
|
|---|
| Project Period (FY) |
2015-04-01 – 2018-03-31
|
| Keywords | ラムダ・ミュー計算 / 古典論理 / 合流性 / カット除去 |
|---|
| Outline of Annual Research Achievements |
昨年度までの成果をもとに，古典論理に対応する計算体系についての研究を行ない，以下の成果を得た．
1. 計算体系の合流性証明のための一般的手法の提案：昨年度までに提案した，Z定理を合成関数に適応する証明手法についてさらなる分析を行なった．この手法が，アカトーリらによる置換規則を含む値呼びラムダ計算，およびその古典論理への拡張である値呼びラムダ・ミュー計算の合流性証明に利用できることを示すことにより，本証明手法の有用性を示した．このテーマについて，群馬大学の藤田憲悦准教授との研究討論を行なった．また，本成果を合流性に関する国際ワークショップにおいて発表した．
2. 古典論理の証明に対する計算論的意味と二重否定変換：ベラルディらによる実現可能性解釈にもとづく古典論理への意味付けと，古典論理の直観主義論理への埋め込みである二重否定変換との関連について調査を行なった．
3. 循環証明体系のカット除去に関する考察：循環証明体系は帰納的に定義された述語を含む論理式に対する帰納法による証明を形式化する証明体系の一つであり，帰納法の仮定の利用を循環構造によって表現する．他の証明体系のように，この体系におけるカット除去定理，およびカット除去手続とその計算論的意味に関する考察を行ない，既存の他の形式化による体系との比較のための，新たな帰納法を含む証明を形式化するための体系としてインデックス付き証明体系を考案した．このテーマについて，東邦大学の木村大輔講師との研究討論を行なった．
|
Research Products
(1 results)
