New development in the matured linear logic research and its applications

成熟线性逻辑研究及其应用的新进展

• 批准号: 15300008
• 负责人: OKADA Mituhiro
• 金额: $ 7.36万
• 依托单位: Keio University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 2003
• 资助国家: 日本
• 起止时间: 2003 至 2005
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-15300008/
• 关键词: logical method; linear logic; formal specification; formal verification; real-time system; proof theory

Linear logical proof theory and semantics theory have been developed and the researches have reached a matured stage to integrate proof theory and semantics theory. In this project we developed a method of integrating proof theory and semantics of linear logic and related logics.We specially developed a method to study proof theoretic properties using this integrated framework, by using a phase semantic techniques, including the relation between "simple logic" and linear logic, uniform and abstract characterizations of cut-eliminations and logical computation models.We also applied the linear logical syntax and semantics to formal verification techniques on real-time system designs and correctness proof techniques on security protocols as well as to computational complexity theory and type-inference theories for programming languages.

线性逻辑证明理论和语义学理论已经发展起来，并且在证明理论和语义学理论的结合方面的研究已经达到了成熟阶段。在这个项目中，我们开发了一种集成线性逻辑和相关逻辑的证明理论和语义的方法，我们特别开发了一种使用这个集成框架研究证明理论性质的方法，通过使用一个阶段语义技术，包括“简单逻辑”和线性逻辑之间的关系，统一和抽象的特征割-我们还将线性逻辑语法和语义应用于真实的系统的形式化验证技术中，安全协议的时间系统设计和正确性证明技术以及程序设计语言的计算复杂性理论和类型推理理论。

项目成果

H.Kushida, M.Okada: "A proof-theoretic study of the correspondence of classical logic and model logic"Journal of Symbolic Logic. 68・4. 1403-1414 (2003)

H.Kushida，M.Okada：“经典逻辑和模型逻辑的对应性的证明理论研究”符号逻辑杂志68・4（2003）。

Completeness and Counter-Example Generations of a Basic Protocol Logic

基本协议逻辑的完整性和反例生成

• 发表时间: 2005
• 期刊: Proceedings of the 6^<th> International Workshop on Rule-Based Programming, Electronic Notes in Theo.Comp.Sci. (to appear)
• 作者: Koji Hasebe;Mitsuhiro Okada
• 通讯作者: Mitsuhiro Okada

Towards New Logic and Semantics : Franco-Japanese Collaborative Lectures on Philosonhv of Logic

迈向新逻辑和语义:法日逻辑哲学合作讲座

• 发表时间: 2006
• 作者: Mitsuhiro Okada;Jocelyn Benoist;Jean-Yves.Girard
• 通讯作者: Jean-Yves.Girard

Cognitive Neuroscience for Deductive Reasoning and Inhibitory Mechanism : On the Belief-Bias Effect

演绎推理和抑制机制的认知神经科学：关于信念偏差效应

• 发表时间: 2006
• 期刊: Reasoning and Cognition, (Keio University Press) 近刊
• 作者: Takeo Tsujii;Mitsuhiro Okada;Shigeru Watanabe
• 通讯作者: Shigeru Watanabe

Linear Logic and Intuitionistic Logic

线性逻辑和直觉逻辑

• 发表时间: 2005
• 期刊: La revue internationale de philosophie No.230
• 作者: K.Hasebe;M.Okada;Mitsuhiro Okada
• 通讯作者: Mitsuhiro Okada