数理論理学セミナーのお知らせ

日時：1月26日（木曜日）１７時から　 場所：東京工業大学 大岡山西８号館 Ｗ棟10階 W1008

【１】 話者：松田直祐（神奈川大） 題目：有限線形クリプキフレームで特徴づけられる論理と古典論理で極小な論理式についての考察 概要： 論理式の命題変数への代入は，命題論理の最も基本的な操作の一つである．この代入操作により論理式間に自然な擬順序が導入できる．古森[1]，鹿島[2]は，中間論理（含意断片）について，以下の問を与えた． 「αが古典論理の中で極小なとき，直観主義＋α は常に古典論理となるか？」 本講演では，この問題に対し，以下の手順で考察を与える． (1)高さ高々nの線形クリプキフレームで特徴づけられる論理に対し，証明システムを与える． (2)高さ2の線形クリプキフレームで特徴づけられる論理は，中間論理の中で古典論理の「すぐ下」に位置する論理である．この事実と，(1)で与えた証明システムを用い，古森-鹿島の問題を考察する． [1] Yuichi, Komori. "Independent axiom systems of minimal formulas for classical logic", In proceedings of the 39th MLG meeting, 2005. [2] Ryo, Kashima. "Problems on axiomatization of intermediate propositional logics", In proceedings of the 39th MLG meeting, 2005.

【２】18時頃から 話者：新屋良磨（東大） 題目：単純型付きラムダ計算のベータ簡約列の長さについて 概要：単純型付きラムダ項の任意のベータ簡約列は有限長である (型付きラムダ計算の強正規化性)ものの、オーダーkの型付きラムダ項 の場合、項のサイズのk重指数の長さになりうることが広く知られている． 一方，どの程度多くのラムダ項がそのように長い簡約列を持つのかはこれまで 明らかになっていなかった．本発表では，型付きラムダ項のアリティと変数の 個数の上限を定数とすると，ほとんど全てのオーダーk型付きラムダ項は(k-2) 重指数的な長さの簡約列を持つことを示す． 発表では、本研究の動機となっている高階モデル検査の計算量の量的解析の問題 にも触れる．本研究は浅田和之 氏，小林直樹 氏，塚田武志 氏との共同研究であり， 成果を纏めた論文が国際会議FoSSaCS'17に採択されている．

------ 本セミナーは定期的に東工大で開催しているものです。 初めて参加を希望される方はご一報ください。 ----- 鹿島 亮 東京工業大学 情報理工学院 数理・計算科学系 [email protected]