2012 Fiscal Year Annual Research Report
| Project/Area Number |
21700014
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
照井 一成 京都大学, 数理解析研究所, 准教授 (70353422)
|
|---|
| Project Period (FY) |
2009-04-01 – 2013-03-31
|
| Keywords | 数理論理学 / 部分構造論理 / エルブランの定理 / 代数的完備化 / ラムダ計算 / 計算量 / 共通型 |
|---|
| Research Abstract |
本研究の目的は、1.部分構造論理の代数的証明論、および2.ルディクスをはじめとするゲーム意味論一般への余代数的アプローチを主眼とするものである。
2.については、昨年度の研究成果である単純型付きラムダ計算の計算量に関する論文"Semantic evaluation, intersection types and complexity of simply typed lambda calculus"が第２３回「書き換え技法とその応用」国際会議(RTA12)にて最優秀論文賞を受賞したことを記すにとどめる。
本年度はもっぱら1.についての研究を行った。(i) 述語部分構造論理の文脈で、エルブランの定理がコンパクトな代数完備化（たとえば正準拡大）に帰着することを示した。さらに超正準拡大という新しいコンパクト完備化法を導入することにより、広範なクラスの論理（FLewに任意のP3公理を付け加えて得られる論理全般）に対してエルブランの定理が成り立つことを代数的に証明した。(ii) 部分構造論理の代数的証明論プログラムの第二主要論文の草稿を書きあげた。現在投稿準備中である。(iii) ファジー論理の証明論でよく知られている稠密性除去定理を代数的に解釈することにより、与えられた有界線形順序構造を論理法則を保ちつつ稠密化する手法を考案した。これにより一群のファジー論理の標準完全性（[0,1]を台とする代数クラスについての完全性）を純粋に代数的に証明することが可能となった。本成果は、証明論の手法が代数の文脈でも直接的な応用を持つことを端的に示しており、代数的証明論の有用性を裏付けるものである。
|
| Current Status of Research Progress |
Reason
24年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
24年度が最終年度であるため、記入しない。
|
