| 研究分担者 |
菊池 誠 神戸大学, 大学院・自然科学研究科, 助手 (60273801)
鹿島 亮 東京工業大学, 大学院・情報理工学研究科, 講師 (10240756)
安本 雅洋 名古屋大学, 大学院・多元数理科学研究科, 助教授 (10144114)
龍田 真 京都大学, 大学院・理学研究科, 助教授 (80216994)
長谷川 立 東京大学, 大学院・数理科学研究科, 助教授 (20243107)
|
|---|
| 研究概要 |
本研究の目的は,ロジックを枢軸として計算機科学と数学の中間領域を開拓し,両分野の交流をさらに活発化させていくことである.この目的のため,本年は以下のような研究活動を行った.
1.次の研究集会の開催を旅費の面でサポートした.
証明論研究会(日大,8月),Workshop on Theories of Types and Proofs(東工大,9月),Workshop on Meta-Arithmetic and Computation(東北大,10月),記号論理学と情報科学(九大,10月).
2.J.Krajicek博士(オックスフォード大)を招聘して講演会を開き,さらに本研究に関するレビューを受けた(9〜10月).
3.田中(研究代表者)が,Logic Colloquium97で研究成果を発表した(7月).長谷川氏が,Advances in Computing Science・ASIAN'97で研究成果を発表した(12月).
主な分担者の研究内容は以下のようである.
田中は,ケ-ニヒの補題に基づく2階算術の体系WKL_0のモデルの性質を調べ,それを応用していくつかの重要定理をWKL_0で導くことに成功した.長谷川氏は,Joyalによる解析関手の理論を用いることで,整列半順序の議論が一つの枠組のなかでユニフォームに展開できることを示した.龍田氏は,フェファーマンの関数およびクラスの構成的論理に対し,q-実現可能性解釈を与えてその健全性を証明し,未解決問題を解いた.安本氏は,限定算術の超準モデルのBool値拡大と計算量理論のP=NP問題との関係について調べた.鹿島氏は,一連の部分構造論理のカット除去等の証明論的性質を詳細に調べた.菊池氏は,PHPの証明図の長さをrandom restrictionの手法を用いて調べた.
|
