プログラム

8月10日（火）

• 10:00–10:10 諸連絡

• 10:10–11:55 セッション１ 座長：中村誠希（東京工業大学）

  • 10:10–10:35 石原豪人

    • 題目：Diagonal Ramsey numbers

    • 概要：TBA(Ramsey数の近似式を求める)

  • 10:35–11:15 高木研斗（東京工業大学）

    • 題目：論理結合子の選択による述語論理の関係への影響

    • 概要：真理値表を持つ一般の論理結合子を扱う古典述語論理、直観主義述語論理、および定領域の論理（CD）を導入し、使用する論理結合子の選択がこれらの論理の間の包含関係に与える影響を明らかにする。

  • 11:15–11:55 福田陽介（千葉工業大学）

    • 題目：A model of intuitionistic modal linear logic

    • 概要：様相論理の線型論理による分解である様相線型論理を直観主義K, T, K4,

S4の必然様相断片について定式化し，対応する型付きラムダ計算およびその表示的意味論を[Barber 1996][Kavvos

2017]の研究を基に与える．

• 11:55–14:10 昼休憩

• 14:10–16:10 セッション２ 座長：福田陽介（千葉工業大学）

  • 14:10–14:50 河野友亮（フェリス女学院大学）

    • 題目：複数観測者のための量子動的認識論理

    • 概要：以前の研究で単一観測者のための量子動的認識論理を構成したが、それを複数観測者のための論理に発展させるには、モデルに根本的な改良が必要であった。
      
      複数観測者間の量子通信等では、エンタングル（量子もつれ）等の、1粒子1観測者の状況では表れてこなかった複雑で重要な概念が登場し、モデルはそれらを扱えるようにしなければならないためである。
      
      今回は、モデルを改良する代わりに、改良しないそのままのモデルと動的認識論理の基本的なモデルを技巧的に組み合わせ、目的のモデルを得た。
      その得られたモデルに対し健全性と完全性の成り立つ演繹体系を構成した。

  • 14:50–15:30 小松弘佳（東京大学）

    • 題目：The Display Calculus and Proof Nets for the Lambek-Grishin Calculus, and Mildly Context-Sensitive Grammars

    • 概要：証明論の論理体系を形式文法として用いる方法であるtypelogical grammarから出発し、シークエント計算の一般化であるdisplay計算によるLambek-Grishin計算の定義と、proof netsによる特徴づけ、そしてそれを用いた弱文脈依存文法と呼ばれる文脈自由文法より広い言語クラスの関連性について話す。

  • 15:30–16:10 間庭彬仁（東京工業大学）

    • 題目：A Modality for Iteration

    • 概要：本発表では nested sequent calculus に基づいて GL と iteration の Curry-Howard 対応を示す.

• 16:10–16:30 小休憩

• 16:30–17:50 セッション３ 座長：竹内泉（産業技術総合研究所）

  • 16:30–17:10 湯山孝雄（東京工業大学）

    • 題目：群の語の問題と言語クラスの閉包性

    • 概要：TBA

  • 17:10–17:50 新屋良磨（秋田大学）

    • 題目：正則言語の局所多様体とそのカラテオドリ拡張

    • 概要：言語クラスCとある言語Lに対して「LがC可測である」とは、LがCの言語でいくらでも良い精度(密度の意味で)で近似できることを言う．

クラスCとして正則言語全体を考えた場合の正則可測性は、もともと話者がとある未解決問題へのアプローチとして考案したものである．

本講演では、正則可測性の動機や具体例を紹介し、さらに、代数的に振る舞いの良い正則言語のある部分クラスCに対するC可即性に

ついての結果を紹介する．本講演は[1]の結果に基づくものである．

[1] Ryoma Sin’ya: Caratheodory Extensions of Subclasses of Regular Languages, Developments in Language Theory (DLT), 2022, to appear.

• 17:50–18:00 諸連絡

8月11日（水）

• 10:00–10:10 諸連絡

• 10:10–12:10 セッション４ 座長：河野友亮（フェリス女学院大学）

  • 10:10–10:50 池田光優（大阪大学）

    • 題目：LTL formulaで定められた性質を連続時間確率過程が満たす確率について

    • 概要：本公演では、連続時間確率過程の経路（見本過程）に対してLTL formulaを定め、Brown運動のような代表的な確率過程がformulaを満たす事象の可測性、及び確率について議論する。

  • 10:50–11:30 只木孝太郎（中部大学）

    • 題目：A refinement of the quantum noiseless channel coding theorem by algorithmic randomness

    • 概要：The notion of probability plays a crucial role in quantum mechanics. It appears in quantum mechanics as the Born rule. In modern mathematics which describes quantum mechanics, however, probability theory means nothing other than measure theory, and therefore any operational characterization of the notion of probability is still missing in quantum mechanics. In our former works, based on the toolkit of algorithmic randomness, we presented a refinement of the Born rule, called the principle of typicality, for specifying the property of the results of quantum measurements in an operational way. In this talk, we make an application of our framework to the quantum noiseless channel coding theorem for refining it, in order to demonstrate how properly our framework works in practical problems in quantum mechanics.

  • 11:30–12:10 吉田聡（公立鳥取環境大学）

    • 題目：構成的解析学における関係の連続性

    • 概要：関数の一般化としての関係について、その連続性を構成的解析学において議論する。

• 12:10–14:10 昼休憩

• 14:10–16:10 セッション５ 座長：新屋良磨（秋田大学）

  • 14:10–14:50 中村誠希（東京工業大学）

    • 題目：ポジティブ関係計算の formula-size game について

    • 概要：ポジティブ関係計算は３変数ポジティブ存在論理と二項関係の表現力に関して等価である一方、表現の簡潔さに関しては指数的な差が生じる。本講演では、ポジティブ関係計算の formula-size game を導入する方法により、３変数ポジティブ存在論理がポジティブ関係計算と比較して指数的に簡潔であることを示す。

  • 14:50–15:30 益岡幸弘（総合研究大学院大学）

    • 題目：帰納的定義付き一階述語論理の循環証明体系におけるカット除去

    • 概要：循環証明体系とはその証明図がサイクル付きの木の形になっている証明体系である．帰納的定義付き一階述語論理の循環証明体系においてカット除去性が成り立たないことを示す．

  • 15:30–16:10 竹内泉（産業技術総合研究所）

    • 題目：強化学習による記号論理の学習

    • 概要：強化学習により記号論理を学習するシステムの数理論理学的な正当性について議論する。

• 16:10–16:20 諸連絡