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

点击翻译按钮获取中文摘要

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