1996 Fiscal Year Annual Research Report
| Project/Area Number |
07808035
|
|---|
| Research Institution | Keio University |
|---|
Principal Investigator |
岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
|
|---|
| Keywords | 線形論理 / Phase Semantics / 並行計算 / 正規化定理 / カット消去定理 / 証明論 |
|---|
| Research Abstract |
線形論理の特徴である(1)並行処理概念の内包、(2)計算資源の消費関係の顕在化、(3)計算状態の顕在化、等を用いた線形論理に基づく種々の新しい計算モデルの構成を行った。特に、(A)Phase Semanticsと呼ばれる線形論理の論理的意味論(「証明可能性」概念のための表示的意味論)をよりダイナミックスな計算過程を表示するための意味論(cut-消去定理や正規化定理を表示できる「証明の正規化」概念のための意味論)へと発展させることに成功した.(B)多項式時間計算量を純粋に論理的に特徴付けるLLL(Light Linear Logic)体系に対する意味論はこれまで未解決であったが、(A)の手法を応用することにより、これに成功した.(C)Proof-searchパラダイムに基づく意味論構成はこれまでの伝統的論理学においてはよく知られた方法であったが、線形論理やsubstructural logics等ではこれまで方法論が確立されていなかった.これに対しても(A)の方法を変形して確立し、それを並行計算の意味論に応用した。
|
-
[Publications] 岡田光弘: "Phase Semantics for Higher Order Completeness,Cut Elimination and Normalization Proofs" Electronic Notes of Theoretical Computer Science. 3. 全23ページ (1996)
-
[Publications] J-P.Jonannand,岡田光弘: "Abstract Data Type Systems" Theoretical Computer Science. (近刊). 全43ページ (1997)
-
[Publications] 浜野正浩,岡田光弘: "A Relationship Among Gentzen's Proof Reduction Kirby-Paris Hydra Game and Buchholz′s Hydra Game" Mathematical Logic Quarterly. 43. 103-120 (1997)
-
[Publications] 浜野正浩,岡田光弘: "A Direct Independence Proofs of Buchholz's Hydra Game on Labeled Finite Trees" Archive for Mathematical Logic. (近刊). (1997)
-
[Publications] 永山 操,岡田光弘: "A Graph-Theoretic characterization of Multiplicative Fragment of Non Commutative Linear Logic" Electronic Notes of Theoretical Computer Science. 3. 全13ページ (1996)
-
[Publications] 岡田光弘: "線形論理に基づく並行計算モデル" 情報処理. 4月号. 327-332 (1996)
-
[Publications] Max Kanovitch,岡田光弘,Andre Scedrov: "Proceedings of International conference on the Mathematical Foundations of Programming Semantics" Springer, 執筆部分全13ページ (1997)
-
[Publications] 岡田光弘: "情報科学のための論理学(近刊)" 産業図書(予定), 273 (1997)
