课题基金 / 基金详情

線形論理の意味論的手法による並行計算概念および実行可能計算量概念の論理的分析

線形論理の意味論的手法による並行計算概念および実行可能計算量概念の論理的分析
使用线性逻辑的语义方法对并行计算概念和可执行复杂性概念进行逻辑分析
批准号：
09878062
负责人：
岡田 光弘
金额：
$1.22万
依托单位：
Keio University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Exploratory Research
财政年份：
1997
资助国家：
日本
项目状态：
已结题
起止时间：
1997 至 1998
来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-09878062/
关键词：
線形論理実現可能計算量実時間システム相意味論完全性定理カット消去定理形式仕様プログラム形式検証セマンティクスタイプ理論並行計算高階論理計算モデル正規化定理

项目摘要

项目成果

岡田 光弘的其他基金

相关文献

中文摘要
翻译
点击翻译按钮获取中文摘要
英文摘要
J-Y.Girardによって1987年に導入された線形論理は計算資源の消費概念、計算状態の変移概念、並行計算概念などを直接論理的に表現し得るまったく新しい論理体系として注目されている。本研究では、実現可能計算量概念を内に含む論理体系としてGirardによって1996年に導入されたLight Linear Logicと呼ばれる線形論理の部分体系に対する意味論的分析の新しい方法論を確立した。これによって、これまで統語論的立場からのみ分析が可能であったLight Linear Logicの実現可能計算量(多項式時間計算量)概念に対して、純粋に意味論的立場からの分析が可能になった。特に、高階相意味論によるLight Linear Logicの完全性定理及び意味論的カット消去定理証明を与えることに成功した。又、これまで研究されてきた線形論理による並行計算プログラミングの枠組に、実時間概念を導入することにより、実時間システムに対する仕様・検証理論を与え、この枠組に対する意味論を確立し、完全性定理を証明すると同時に、実時間システムの安全性等の検証問題がPSPACE決定可能なことを示した。
期刊论文(0)
专著(0)
科研奖励(0)
会议论文
M.Takahashi-M.Okada-M.Dezani(eds.): "Theories of Types and Proofs" Mathematical Society of JAPAN(日本数学会), 297 (1998)
M.Takahashi-M.Okada-M.Dezani（编）：“类型和证明的理论”日本数学会，297（1998）
DOI： --
发表时间：
期刊：
影响因子： --
作者： []
通讯作者：
M.Hamano, M. Okada: "A Relationship Among Gentzen'S Proof Reduction, Kirby-Paris Hydra Game and Buchholz's Hydra Game"Mathematical Logic quarterly. 43. 103-120 (1997)
M.Hamano、M. Okada：“Gentzen 证明还原、Kirby-Paris Hydra Game 和 Buchholzs Hydra Game 之间的关系”数理逻辑季刊。
DOI： --
发表时间：
期刊：
影响因子： --
作者： []
通讯作者：
M.Hamano-M.Okada: "A Direct Independence Proof of Buhholz's Hydra Game" Archiev for Mathematical Logic. (to appear). (1998)
M.Hamano-M.Okada：《布霍尔茨九头蛇博弈的直接独立性证明》Archiev，数学逻辑。
DOI： --
发表时间：
期刊：
影响因子： --
作者： []
通讯作者：
M.Kanovitch-M.Okada -A.Scedrov: "Specifying Real-Time Finits State Systems by Linear Logic" Electronic Notes of Theoretical Computer Science. 16(1998). 1-14 (1998)
M.Kanovitch-M.Okada -A.Scedrov：“通过线性逻辑指定实时有限状态系统”理论计算机科学电子笔记。
DOI： --
发表时间：
期刊：
影响因子： --
作者： []
通讯作者：
共 15 条
    論証・証明の哲学の深化に向けた学際的「論理の哲学」研究
    • 批准号：
      23K20416
    • 项目类别：
      Grant-in-Aid for Scientific Research (B)
    • 资助金额：
      $3.24万
    • 财政年份：
      2024
    • 负责人：
      岡田 光弘
    • 依托单位：
      Keio University
    On information presentation methods for easier decison making: Studies on multi-attribute decision making
    • 批准号：
      21K18339
    • 项目类别：
      Grant-in-Aid for Challenging Research (Exploratory)
    • 资助金额：
      $4.08万
    • 财政年份：
      2021
    • 负责人：
      岡田 光弘
    • 依托单位：
      Keio University
    Interdisciplinary studies on philosophy of logic: Toward the development of philosophy of proof and demonstration
    • 批准号：
      21H00467
    • 项目类别：
      Grant-in-Aid for Scientific Research (B)
    • 资助金额：
      $8.49万
    • 财政年份：
      2021
    • 负责人：
      岡田 光弘
    • 依托单位：
      Keio University
    Study on "Disagreement" in logic
    • 批准号：
      19KK0006
    • 项目类别：
      Fund for the Promotion of Joint International Research (Fostering Joint International Research (B))
    • 资助金额：
      $7.49万
    • 财政年份：
      2019
    • 负责人：
      岡田 光弘
    • 依托单位：
      Keio University