プログラム
9月11日(日)
13:00 ~ 13:15
オープニング+連絡など
13:15 ~ 13:45
西澤弘毅(神奈川大学)
演題:Priestley duality from opfibrations and fibrations
梗概:ストーン双対性は、ある代数たちの圏とある位相空間たちの圏の間の反変圏同値であり、その本質的な情報は双対随伴の中にある。昨年の発表では、位相に関する議論なしでこの双対随伴を得ることを目的とし、代数と付加的なパラメータを基に、形式空間という抽象的な位相空間を構成する方法を示した。通常の位相空間はその例になる。今回の発表では、その理論を拡張することによって、プリーストリー双対性も構成できたことを報告する。
13:45 ~ 14:15
田中康平(信州大学)
演題:Topological motion planning on stratified spaces
梗概:カーナビゲーションや自動運転技術を支えるシステムの根幹には,動作領域上の2点が与えられた際に,それらを繋ぐパスをどのように指定するかという問題がある.本研究では,分割された領域上で境界を跨がない経路指定に限定し,領域全体で移動を制御するためには,最低何種類の経路指定アルゴリズムが必要かを考える.
14:30 ~ 15:30
松田直祐(新潟工科大学)
演題:直観主義論理とKripke意味論とBool関数の関数的完備性
梗概:Bool関数の集合Fが(古典意味論上で)関数的完備であるとは,どんなBool関数fに対しても,fと同等な(古典意味論上で)論理式をFの関数を組み合わせて与えられる時をいう。Fが関数的完備であるための必要十分条件は1942年にPostにより与えられている。本講演ではKripke意味論上での関数的完備性を考え,Bool関数の集合FがKripke意味論上で関数的完備であるための必要十分条件を,Postの条件を拡張する形で与える。
15:45 ~ 16:15
間庭彬仁(東京工業大学)
演題:Nested modal λ-calculi
梗概:本発表では,nested sequent calculus のアイディアに基づいた様相論理の natural deduction を与え,そられの Curry-Howard 対応について考える.
16:15 ~ 16:45
新屋良磨(秋田大学)
演題:局所的な性質で記述できる正規言語部分クラスについて
梗概:本講演では,正規言語(単項二階述語論理で定義可)のいくつかの部分クラス(星無し言語,局所検査可能言語,etc)について背景や理論を紹介し,講演者の研究テーマである可測性に関する結果と未解決問題を報告する.
9月12日(月)
10:00 ~ 10:30
小川瑞史(JAIST)
演題:On axiomatization of graphs with bounded tree width
梗概:Inspired by the complete axiomatization of series-parallel graphs (Pous, et.al 2018), we try to extend it to graphs with tree width k by using SP term construction (Ogawa, et.al. 2003).
10:30 ~ 11:00
西村進(京都大学)
演題:認識論理による分散タスク不可解性とその証明能力について
梗概:分散タスクの不可解性、すなわち与えられた分散計算タスクが特定の分散システムで実現不可能であることを示すには単体的複体モデルを用いた幾何的手法が有効であることがよく知られている。近年Goubaultらによって、複体モデルから導出した認識論理のKripkeモデル上で可解性に矛盾する障害論理式を発見することによっても不可解性証明が可能であることが示された。しかしながら現在のところ、障害論理式の実例はあまり知られていない。
本講演では、認識論理の障害論理式の存否が、異なる認識論理言語(知識様相の種類や命題不動点の有無)や分散システムの計算力(1ラウンド/多ラウンドプロトコル)の組合せでどう変わるかについての現時点での知見を、講演者の最近の結果も交えながら紹介する。また、分散タスク不可解性に対して認識論理を用いることの有効性についても考察する。
11:00 ~ 11:30
中村誠希(東京工業大学)
演題:ハイパーエッジ置換文法のための空間ポジティブ存在論理について
梗概:本発表では、ハイパーグラフ言語のための空間意味論およびこの意味論に基づくポジティブ存在論理式とハイパーエッジ置換文法の間のいくつかのKleeneの定理(表現可能な言語のクラスが一致すること)について、 (Nakamura 2022) に基づき紹介する。
11:30 ~ 11:45
クロージング+連絡など