ジラールの線形論理とその情報科学への応用

1995 年度 実績報告書

• 研究課題/領域番号: 07808035
• 研究種目: 一般研究(C)
• 研究機関: 慶応義塾大学
• 研究代表者: 岡田 光弘 慶應義塾大学, 文学部, 助教授 (30224025)
• キーワード: 線形論理 / 正規化定性 / 並行計算 / プログラミング言語

研究概要

線形論理の基礎理論及び応用を与えた。基礎論理に関しては、Phase Semanticsの高階線形論理への応用及びPhase Semanticsの強正規化定性(Strong Normalization Theorem)への応用を与えた。又、線形論理のNon-commutativeなversionに対するProof Netsのグラフ論的な特徴付け定理を与え、グラフ論的なPlanityの概念と線形論理のNon-commutativityの概念との間の正確な関係を明かにした。
応用面に関しては、線形論理の並行計算モデルへの応用及び線形論理の論理型プログラミング言語理論への応用を与えた。特に、並行プロセスと線形論理のfragmentとの間の完全性、Horn-fragmentとPetri nets modelsとの間の完全性、等を与えた。

研究成果

• [文献書誌] 岡田光弘(Jouannaudとの共著): "Abstract Data Type Syotems" Theoretical Computer Science. 近刊. (1996)
• [文献書誌] 岡田光弘(永山との共著): "A Graph-theoretic characterization for non-commutative Multilicative Linear Logic" Electronic Notes of Theoretical Computer Science (ヨーロッパ理論情報学会). 3. 11 (1996)
• [文献書誌] 岡田光弘: "From Phase Semantics to Normalization Proofs, Part I" Electronic Notes of Theoretical Computer Science (ヨーロッパ理論情報学会). 3. 10 (1995)
• [文献書誌] 岡田光弘(浜野と共著): "A Direct Proof of Buchnolz's Hydra Game on Labeled Finite Trees" Archiev for Mathematical Logic. 近刊. (1996)
• [文献書誌] 岡田光弘(浜野と共著): "Relationship Among Gentzen's Reduction, Kirby-Paris' Hydra Game and Buchholz's Hydra Game" Mathematical Logic Quarterly. 近刊. (1996)
• [文献書誌] 岡田光弘: "線形論理に基づく平行計算モデル" 情報処理(特集記事). 4月号. 6 (1996)
• [文献書誌] 岡田光弘: "情報科学のための論理" 産業図書, 240 (1996)
• [文献書誌] 岡田光弘: "Special Issue on Linear Logic (editor), Electronic Notes of Theoretical Computer Science" Elsevier社(オランダ)[ヨーロッパ理論情報学会編], 420 (1996)