所員 -照井 一成-
名前
照井 一成 (Terui, Kazushige)
照井 一成 (Terui, Kazushige)
職
准教授
准教授
E-Mail
terui （emailアドレスには＠kurims.kyoto-u.ac.jp をつけてください）
terui （emailアドレスには＠kurims.kyoto-u.ac.jp をつけてください）
研究内容
数理論理学に関する研究
数理論理学に関する研究
紹 介
「古典論理を理解するための非古典論理学」を推進する一方，
計算量，プログラムの意味，評価戦略など，計算機科学にまつわる諸問題を
数理論理学によって解明することを目指している。かつて論理学といえば
「真なる命題→真なる命題」という推論の研究に範囲が限定されていたが，
現代においては「インプット→アウトプット」という計算や，
「エージェント⇔エージェント」というコミュニケーションをも
十分視野に納めている。特に関心をもっているのは，
（１）線形論理と（２）部分構造論理である。
（１）線形論理，これは数学において線形代数が果たすのと同じ役割を 論理学において果たすものである。証明やプログラムは 線形的な部分と指数関数的な部分に分解できるというのがその核心である。 これまでは，線形論理に基づく計算量クラスの特徴付け[5,7,8]，線形論理から派生 したルディクス（あそび）の理論に基づく計算論再構築の試みなどを行ってきた[4]。ルディクスのフレームワークは多くの可能性を秘めており，伝統的な完全性定理（証明可能性 vs 反証可能性）をルディクスに基づいて証明-モデル間のコミュニケーションとして理解する試み[3], 再帰型の一意的解釈[1]等の研究を進めている。 他にもたとえばゲーデルの不完全性定理をコミュニケーションの観点から見るとどうなるのか，無限構造上のオートマトンに関する決定問題はどうか，対話的計算量クラスはどうか，など興味の尽きるところがない。
（２）部分構造論理，これは構造規則を弱めることによって得られる 論理一般の系を考察することにより論理の本質に迫ろうという試みである。 主な成果としては，まず与えられた部分構造論理（シークエント計算）について 証明論の基本定理（”補題を用いて間接的に証明できることは直接的にも証明できる” こと） が成り立つための必要十分条件を代数的に与えたことがあげられる[9,10]。現在提唱 しているのは， 非古典論理における代数的証明論のプログラムであり，これはさまざまな論理的公理 を 証明論的難易度に従って階層づけ，そして証明論的手法と代数的手法の相互作用を通 じて 新しいタイプの結果を出していこうというものである[2,6]。鍵となるのは，証明論の 基本定理は 代数の言葉でいえば完備化に相当するという洞察である。これにより証明論的研究と 代数的研究を結び付けることが可能になり，部分構造論理一般の可能性と限界を画定 するという 目標が一気に現実味を帯びてきた。当面この方針に従って研究を進める予定である。
（１）線形論理，これは数学において線形代数が果たすのと同じ役割を 論理学において果たすものである。証明やプログラムは 線形的な部分と指数関数的な部分に分解できるというのがその核心である。 これまでは，線形論理に基づく計算量クラスの特徴付け[5,7,8]，線形論理から派生 したルディクス（あそび）の理論に基づく計算論再構築の試みなどを行ってきた[4]。ルディクスのフレームワークは多くの可能性を秘めており，伝統的な完全性定理（証明可能性 vs 反証可能性）をルディクスに基づいて証明-モデル間のコミュニケーションとして理解する試み[3], 再帰型の一意的解釈[1]等の研究を進めている。 他にもたとえばゲーデルの不完全性定理をコミュニケーションの観点から見るとどうなるのか，無限構造上のオートマトンに関する決定問題はどうか，対話的計算量クラスはどうか，など興味の尽きるところがない。
（２）部分構造論理，これは構造規則を弱めることによって得られる 論理一般の系を考察することにより論理の本質に迫ろうという試みである。 主な成果としては，まず与えられた部分構造論理（シークエント計算）について 証明論の基本定理（”補題を用いて間接的に証明できることは直接的にも証明できる” こと） が成り立つための必要十分条件を代数的に与えたことがあげられる[9,10]。現在提唱 しているのは， 非古典論理における代数的証明論のプログラムであり，これはさまざまな論理的公理 を 証明論的難易度に従って階層づけ，そして証明論的手法と代数的手法の相互作用を通 じて 新しいタイプの結果を出していこうというものである[2,6]。鍵となるのは，証明論の 基本定理は 代数の言葉でいえば完備化に相当するという洞察である。これにより証明論的研究と 代数的研究を結び付けることが可能になり，部分構造論理一般の可能性と限界を画定 するという 目標が一気に現実味を帯びてきた。当面この方針に従って研究を進める予定である。
- Michele Basaldella and Kazushige Terui. Infinitary completeness in ludics. Proceedings of IEEE Annual Symposium on Logic in Computer Science (LICS'10), pp. 294-303, 2010.
- Agata Ciabattoni, Lutz Stra\ss burger and Kazushige Terui. Expanding the realm of systematic proof theory. Proceedings of Computer Science Logic (CSL'09), pp. 163-178, 2009.
- Michele Basaldella and Kazushige Terui. On the meaning of logical completeness. Proceedings of Typed Lambda Calculus and Its Applications (TLCA'09), pp. 50-64, 2009.
- Kazushige Terui. Computational ludics. Theoretical Computer Science, 412, Issue 20, pp. 2048-2071, 2011.
- Patrick Baillot and Kazushige Terui. Light types for polynomial time computation in lambda calculus. Information and Computation, 207, No. 1, pp. 41-62, 2009.
- Agata Ciabattoni, Nikolaos Galatos, and Kazushige Terui. From axioms to analytic rules in nonclassical logics. Proceedings of IEEE Annual Conference on Logic in Computer Science (LICS'08), pp. 229-240, 2008.
- Vincent Atassi, Patrick Baillot, and Kazushige Terui. Verification of ptime reducibility for system F terms: Type inference in dual light affine logic. Logical Methods in Computer Science, 3, No. 4, 2007.
- Kazushige Terui. Light affine lambda calculus and polynomial time strong normalization. Archive for Mathematical Logic, 46, No. 3-4, pp. 253-280, 2007.
- Kazushige Terui. Which structural rules admit cut elimination? An algebraic criterion. Journal of Symbolic Logic, 72, No. 3, pp. 738-754, 2007.
- Agata Ciabattoni and Kazushige Terui. Towards a semantic characterization of cut-elimination. Studia Logica, 82, No. 1, pp. 95-119, 2006.