yf [at] lambda.ski ）以下はSLACSのページの冒頭からの抜粋です．
SLACS（スラックス）は，記号論理学と情報科学の境界領域に関する研究発表・研究討論の場を提供することを目的にして開催されている研究集会です．1985年1月に第１回が開催されて以来，毎年１回のペースで開催されています．SLACSは，堅苦しい研究会ではなく，その年の幹事を中心とした参加者自らの手作りによるフレンドリーな雰囲気を持った集会です．気軽に発表できる場ですから，研究が進行中の話題を持ってきて議論したり，学生さんが発表する場としても適当です．もちろん，発展を続けるこの分野の最先端の研究テーマに関する発表も数多く聞くことができます．参加者の資格は問いませんので，原則として，どなたでも講演発表・聴講いただけます．発表はごく少数の例外を除いて日本語です．
研究集会への参加を希望の方は以下の Microsoft Forms のフォームより登録をお願いします．参加申し込みは 開催前日まで受け付けます 会期中も含めて随時受け付けます（申込時のEメールアドレスに対してオンライン参加のための情報が自動返信されます）．
講演申込みについては2023年8月21日時点で締め切りました．
プログラム中に断りのない限り，講演は対面発表で40分間（質疑・発表切り替わりの時間を含む）の発表です．
カリー・ハワード同型において様相論理の証明体系が多段階計算の型システムとして解釈できることが知られている。本講演ではラベル付き演繹を用いて様相演算子を一般化したラベル付き様相を定義し、これを多段階計算において変数スコープをコードの型に明示する Refined Environment Classifiers の手法に対応する論理的基礎として解釈する試みについて現在の進捗を説明する。
TBA
論理定項ΩはHumberstoneにより[1]ではじめて直観主義論理に加えられ、[2]でこの論理のヒルベルト公理系の提供や他の論理との比較がなされた。論理定項Ωは、一点生成される半順序関係をもつ直観主義論理のクリプキモデル上に加えられ、最小元ではボトム、それ以外の状況ではトップとしてふるまう。すでに[1]で述べられているように、直観主義論理に論理定項Ωを加えると、演繹定理は不成立となるが、含意とΩを用いることで古典論理における否定が定義できる。先述したように、論理定項Ωは半順序関係をもつクリプキモデルを前提とするが、通常の直観主義論理では、擬順序関係を用いてもクリプキモデルを定義できることが知られている。ゆえに、論理定項Ωを一点生成される擬順序関係をもつ直観主義論理のクリプキモデル上に加えた場合、どのような成果が得られるか、という問いを立てることができる。本発表では、この問いについて二つの成果を示す。一つ目は論理定項Ωを用いることで、根の極小性と呼ばれる性質を定義する論理式を与えることができるという点である。このような論理式は、通常の直観主義論理の言語では提供不可能である。二つ目は、擬順序関係をもつクリプキ意味論と半順序関係をもつクリプキ意味論で同じ論理を定義するためには、論理定項Ωの充足関係の定義を[1]と[2]で用いられているものから、変更する必要があることを示す点である。具体的には、従来のΩの充足関係の定義では、擬順序関係をもつクリプキモデルを、半順序関係をもつクリプキモデルに変更できないことを示し、この変形を可能とする新しいΩの充足関係を提供する。
※本研究は佐野勝彦氏（北海道大学）との共同研究である
[1] Humberstone, L. Extensions of intuitionistic logic without the deduction theorem: Some simple examples. Reports on Mathematical Logic, Volume 40, pp.45-82, 2006.
[2] Niki, S and Omori, H. A note on Humberstone’s constant Ω. Reports on Mathematical Logic, Volume 56, pp.75-99, 2021.
無向グラフは、非反射性と対称性を持つ Kripke frame と考えることができる（Goldblatt (1974) はこれを orthoframe と呼んでいる）。本発表では、これに対応する hybrid logic を IB(@) と呼び、その tableau calculus を与える。 その後、 IB(@) の tableau calculus について orthoframe との完全性を示す。さらに、 tableau calculus において重要な性質である、任意の tableau が有限の長さしかもたないという性質（停止性）も証明する。
※本研究は、高木翼（JAIST）との共同研究である。
卒業研究の学生たちと共に開発しているソフトウェアにおいて、複雑な構造を持つ状態をできるだけメモリ効率の良い方法で、しかもできるだけ簡潔なコーディングで更新する手段が必要になった。本講演ではそのために採用したシンプルだが効果的な手法について述べる。
代数的エフェクトとエフェクトハンドラは、適当なモナドに対応する副作用を取り扱うためのプログラミング言語の機構である。本発表ではアローと呼ばれる副作用を捉える概念に対する代数的エフェクトとエフェクトハンドラを考察し、その操作的意味論および表示的意味論を与える
代数的エフェクトとハンドラを持つ言語の既存のエフェクトシステムは，項の評価時に発生しうるエフェクトをどう表現するかという点で大きく異なる．本研究ではエフェクトの表現方法及びエフェクト上の操作を抽象化し，集合や列といった表現方法を採用しているエフェクトシステムへの具体化が可能なエフェクトシステムを与えた．さらに，我々の定義した Safety Conditions という条件を満たすインスタンスは全て型安全であることを示し，複数の設定のもとでこの Safety Conditions を通してエフェクト表現に要求される性質を形式化した．
なお，本研究は関山太朗 (国立情報学研究所) ，五十嵐淳 (京都大学) との共同研究である．
Girardによる線形論理、あるいはその変種となる論理について、計算量と関連付けられたものが存在する。これらは計算量に限らず、計算資源の使用などと関連付けられて、いくつかのプログラミング言語への実装も含め、様々な発展が存在する。一方、これらの論理や言語は時間計算量に対して研究されたものがほとんどで、空間計算量について調べられたものはとても少ない。本講演では空間計算量と関連付けられるような注釈や指標を持つ論理体系（あるいは計算体系）の探求について、現在までに分かっていることを紹介する。
The notion of probability plays a crucial role in quantum mechanics. It appears 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 an operational refinement of the Born rule, called the principle of typicality, for specifying the property of the results of quantum measurements in an operational way. The von Neumann measurement scheme is a quantum-mechanical description of a measurement process as the interaction between a system being measured and an apparatus measuring it, and plays a fundamental role in the principle of typicality. In this talk, we derive the von Neumann measurement scheme without using the Born rule, but based only on the so-called eigenvalue-eigenstate link for a measurement which is certain to give one particular outcome (instead of giving one or other of several possible outcomes, as is in general the case). This result consolidates the foundations of the principle of typicality.
命題 STIT 論理は Horty [1], Belnap et al. [2] により開発された行為ないし選択についての論理である。（時相演算子なしの）命題 STIT 論理は、Kripke 意味論の観点からは、行為者独立性と呼ばれる性質を満たす多様相命題論理 S5 のフレームのクラスに関して完全となる論理である [3]。この論理は行為についての様々な性質を表現することができるが、命題論理をベースとしているため「誰もが A となるようにする」等の量化文を表現することができない。そこで本発表では、行為者独立性を満たす量化多様相論理 S5 のフレームを定義して、このフレームのクラスに関して完全となる量化STIT論理を与えるための予備的考察を行う。
[1] J. F. Horty, Agency and Deontic Logic. Oxford University Press, 2001.
[2] N. Belnap, M. Perloff, and M. Xu, Facing the Future: Agents and Choices in Our Indeterminist World. Oxford University Press, 2001.
[3] A. Herzig and F. Schwarzentruber, “Properties of Logics of Individual and Group Agency,” Advances in Modal Logic, vol. 7, pp. 133–149, 2008.
Integral (resp. square-increasing) commutative residuated lattices は，直観主義線形論理の様相無し断片に弱化規則 (resp. 縮約規則) を加えたものに対応する代数的意味論である．Blok-van Alten [1] は integral commutative residuated lattices のクラス ($\mathbb{ICRL}$) が有限埋め込み可能性 (finite embeddability property) を持つことを示した．この性質は $\mathbb{ICRL}$（より一般には有限公理化可能な代数のクラス）の全称理論 (universal theory) および準等式理論 (quasi-equational theory) の決定可能性を保証する．$\mathbb{ICRL}$ の全称理論と準等式理論がPSPACE-困難であることは予てから知られていたが (cf. [2])，近年 [6] は Lazić-Schmitz [3] の手法を用いることで $\mathbb{ICRL}$ の準等式理論が Schmitz [5] の $\mathbf{F}_3$（計算時間が入力長の初等関数階建ての指数タワーで抑えられる問題のクラス）において完全であることを示した．これは全称理論が$\mathbf{F}_3$-困難であることをも保証する．他方で square-increasing commutative residuated lattices のクラス ($\mathbb{SCRL}$) 上の問題に関しては van Alten-Raftery [8] および Urquhart [7] の仕事が知られている．前者は $\mathbb{SCRL}$ が有限埋め込み可能性を持つことを示したが，それに先んじて後者は $\mathbb{SCRL}$ の（準）等式理論が非原始再帰的（Schmitz [5] による非初等的計算量クラスの階層の言葉で言えば，$\mathbf{F}_{\omega}$-完全）であることを証明した．この結果はさらに $\mathbb{SCRL}$ の全称理論の$\mathbf{F}_{\omega}$-困難性を導く．発表では，$\mathbb{ICRL}$ と $\mathbb{SCRL}$ が全称理論に関してそれぞれ$\mathbf{F}_3$と$\mathbf{F}_{\omega}$で決定可能であることの短い証明を与える．これらは McKinsey [4] のテクニックをはじめとして既存の結果を組み合わせることでごく簡単に示される．
[1] Willem J. Blok and Clint J. van Alten. The finite embeddability property for residuated lattices, pocrims and BCK-algebras. Algebra Universalis, 48:253–271, 2002.
[2] Rostislav Horčík and Kazushige Terui. Disjunction property and complexity of substructural logics. Theoretical Computer Science, 412(31):3992–4006, 2011.
[3] Ranko Lazić and Sylvain Schmitz. Nonelementary complexities for branching VASS, MELL, and extensions. ACM Transactions on Computational Logic, 16(3):20:1–20:30, 2015.
[4] J. C. C. McKinsey. The decision problem for some classes of sentences without quantifiers. The Journal of Symbolic Logic, 8:61-76, 1943.
[5] Sylvain Schmitz. Complexity hierarchies beyond elementary. ACM Transactions on Computation Theory, 8(1):1–36, 2016.
[6] Hiromi Tanaka. Tower-complete problems in contraction-free substructural logics. In Proceedings of CSL 2023, pages 34:1–34:19, 2023.
[7] Alasdair Urquhart. The complexity of decision procedures in relevance logic II. The Journal of Symbolic Logic, 64(4):1774–1802, 1999.
[8] Clint J. van Alten and James G. Raftery. Rule separation and embedding theorems for logics without weakening. Studia Logica, 76(2):241–274, 2004.
定理証明支援系Coqの証明を大規模言語モデルに書かせることにより，定理の検証の自動化を目指す．具体的には，大規模言語モデルにCoqのスクリプトとその応答を入力とし，次のCoqのプログラムを正解の出力として学習させる．Coqのプログラムが書けるか検証する．
山科駅の京阪バス乗り場から「26A系統」のバスに乗車で京都橘大学まで来られます．所要時間は約18分です．各日程で，以下のいずれかの時刻での出発がお勧めです．
なお，会期中は大学の学休期間のためバスの本数が少なくなっています（ノンストップの系統が出ていません）のでご注意ください．
8月31日（木）の18:30から「レストラン菊水」（〒605-0076 京都市東山区四条大橋東詰祇園）の屋上ビアガーデンにて懇親会を行います． 8月24日現在，席に若干名の空きがあるため参加を希望される場合は下記フォームからお申し込みください．2023年8月28日(月)の正午まで申し込みを受け付けますが，申込多数の場合はお断りする場合がありますので参加を希望される場合は早めに登録をお願いいたします．
なお，研究集会会場の京都橘大学から離れた場所での開催ですのでご注意ください．
京都橘大学が位置する京都市山科区はホテルがあまりありません．遠隔地から参加する場合の宿泊場所については以下から確保することをお勧めします．
より詳しい情報はSLACSのページをご確認ください．
Last modified: 02:47 UTC, Sep 04, 2023.