2006 Fiscal Year Annual Research Report
| Project/Area Number |
18740047
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
GALATOS Nikolaos 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (70422665)
|
|---|
| Keywords | 数理論理学 / 代数学 / 情報基礎 |
|---|
| Research Abstract |
本補助金で多くの研究者たちと共同研究をすることができた。彼らと非常に有意義な議論を行ったことにより私のプロジェクトの中で掲げていた多くの目標を達成することができた。(具体的には目標♯1,♯2,♯4)現在においてはプロジェクト♯3の目標を達成するため研究を行っているところである。
#4の目標を達成するため、部分構造論理のために関係意味論を開発した。これらは論理的または代数的システムの間で一般的抽象的な骨組みを提供した。また、代数モデルはSequent計算と同様にそのような意味論の例を提供した。決定可能性への適用により、上記のような関係意味論を#1の目標を達成するために用いた。特に、意味論的な方法においてInFLシステムのcut除去定理(別名purenon-commutative MALL)を証明することができた。
証明探索は終了していないが、システムの決定可能性とより強力なその有限モデル特性を証明することができた。
構造的ルールの説明がCut除去定理を認めることにより、その他の部分構造論理についても似たような結果が得られた。
♯2に関して、代数的完成の論理的意味を研究することができた。同様の類似完成は意味論的Cut除去定理を与え、また、代数的意味論のためのDedekind-MacNeille completionsを専門化した。これにより、すべての簡単な方程式(実際には順応水準は異なるが)Dedekind-MacNeille completionsの下で維持されるということが証明できた。
|
