算術体系の無矛盾性証明におけるゲーデル解釈の論理的・数理哲学的研究

证明算术系统一致性的哥德尔解释的逻辑/数学哲学研究

• 批准号: 01J04474
• 负责人: 長谷部 浩二
• 金额: $ 0.77万
• 依托单位: Keio University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for JSPS Fellows
• 财政年份: 2001
• 资助国家: 日本
• 起止时间: 2001 至 2002
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-01J04474/
• 关键词: 帰納的汎関数体系; 線形論理; セキュリティ・プロトコル

前年度まで行ってきたゲーデルの汎関数体系Tの拡張の試みや線形論理的手法を用いたその応用の試みに対し,本年度は,前年度で得られた研究成果をもとにその計算論的性質(特に重要な性質であるチャーチ・ロッサー性と強正規化性)について考察を行うとともに,その応用についても考察した.(以上で述べた計算論的性質に関する考察は,現在論文等の形で発表するための準備を行っている.)特に近年,理論情報科学において,情報通信を行う上でのセキュリティ確保の技術を論理学的手法を用いて理論的側面から考察する試み(セキュリティ・プロトコルと呼ばれる)が非常に盛んに行われており,本研究で扱われている型理論の手法がこの分野の研究に対しても有効であることが知られている.本年度はこのセキュリティ・プロトコルの分野への本研究テーマの応用を試みた.本年度は上記で得られた成果をもとに,線形論理的手法と信念論理の手法を組み合わせたセキュリティ・プロトコルの検証理論を考察した.この研究で得られた成果は,2002年5月に神戸大学にて行われた学会「人工知能と知識処理」(電子情報通信学会主催)及び同年10月に慶應義塾大学にて行われた国際会議"International Symposium on Software Security"にて岡田教授と共同で口頭発表を行っている.またこれらの結果は論文でProceedingsに収録されている(詳しくは「研究発表」欄を参照).

The previous year's test line shape theory The techniques used are the same as the ones used in the current year and the previous year’s ones. The result of the research is the properties of computational theory (special and important properties) (Strong regularization property) (The above-mentioned properties of computational theory have been investigated, and now the paper is in the form of a table and ready to go.) Special features: In recent years, theoretical information science The hand of information and communication technology Side view of the method and application theory This research is based on the theory of the で扱われている type The method of dividing the field and the research on it are effective and effective. Annual research project of the year Try it out. This year’s results are recorded in the above list, including linear theory techniques and beliefs. An examination of the theory of theory and practice The result of the research was completed by Kobe University in May 2002. "Artificial Intelligence and Knowledge Processing" of the Institute of Science and Technology (organized by the Society of Electronic Information and Communications Technology) and the International Conference "International" held by Keio University in October of the same year Symposium on Software Security "Professor Okada's joint oral examination list. The results of the paper's Proceedings are included in the paper (refer to the "Research Report" column for details).

项目成果

岡田光弘, 長谷部浩二: "線形論理に基づいたセキュリティ・プロトコルの論理的検証法"電子情報通信学会「人工知能と知識処理」研究報告. 102.91. 49-54 (2002)

Mitsuhiro Okada，Koji Hasebe：“基于线性逻辑的安全协议的逻辑验证方法”IEICE“人工智能与知识处理”研究报告102.91（2002）。

Koji Hasebe, Mitsuhiro Okada: "A Logical Verification Method for Security Protocols Based on Linear Logic and BAN Logic"Software Security (Hot topic Series of Lecture Notes in Computer Science). No.2609. 422-445 (2003)

Koji Hasebe、Mitsuhiro Okada：《一种基于线性逻辑和BAN逻辑的安全协议的逻辑验证方法》软件安全（计算机科学热门话题系列讲义）。