第29回記号論理と情報科学研究集会 (SLACS 2012) は，京都産業大学むすびわざ館で開催の予定です．SLACSは，記号論理学とコンピュータ科学の研究者や学生の相互交流を目的として開催されている研究集会で毎年持ち回りで行われています（http://www.math.s.chiba-u.ac.jp/SLACS/）。完成された研究のみならず，発展途上の話題やサーベイなども大歓迎です．記号論理以外にも，圏論やアルゴリズム理論などコンピュータ科学に関わる講演を広く行います。
開催日：2012年9月15日（土）13:00 〜 9月16日（日）18:00
場所：京都産業大学むすびわざ館3階3-B会議室
〒600-8533 京都市下京区中堂寺命婦町1-10
Tel.075-277-1600 Fax.075-277-1699
（京都産業大学神山キャンパスとは異なります）
http://www.kyoto-su.ac.jp/outline/shisetsu/musubiwaza
アクセス：最寄り駅はJR丹波口駅および阪急大宮駅
http://www.kyoto-su.ac.jp/outline/shisetsu/musubiwaza/access.html
研究会参加について申し込みも費用も不要です（懇親会については後述）。皆様ふるってご参加よろしくお願いいたします。なお，本研究集会は科研費（24320008）の助成を受けております。
懇親会は9月15日18:00-20:00に予定しています．
かごの屋五条七本松店
075-326-1165
http://www.kinrei.com/shop/spec/?shop_id=42
http://r.gnavi.co.jp/k539974/（ぐるなび）
懇親会の参加・不参加については事前に世話人に連絡して頂けると助かります。（9/15の15:00頃に人数を確定して私が店に連絡致します。予算3-4千円程度）。
プログラムと梗概については以下をご覧下さい。 現在まだ，題目・梗概が未定の方は連絡をよろしくお願い致します。世話人：
9/15（土曜日）
13:00-13:30
鴨浩靖，萩尾由貴子，溝口涼子（講演者）（奈良女子大学理学部）
題目：三角形に関する平面ユークリッド幾何への数式処理の応用
梗概：未定
13:35-14:05
吉村和人（JAIST）
題目：オラクルの圏論的記述―終対象の一般化として―
梗概：TTE (Type-2 Theory of Effectivity) は計算可能解析学の枠組みの一つである．TTEでの初等的な事実の一つとして，(計算可能性概念の導入された) ある種の位相空間の間の写像に対してはオラクル計算可能性と位相的連続性が一致するというものがある．本発表では左記事実の圏論的特徴づけについて現状得られている結果の紹介を行う ．具体的には，factorization systemを伴う圏のうち適当な性質を満たすものの上で: オラクルの概念の再現; オラクル計算可能性と位相的連続性の一致に相当する命題の特徴づけ: 左記2点を吟味する．
14:10-14:40
江口直日（東北大学理学研究科）
題目：Rewriting Apploaches to Computational Complexity and
Complexity Analysiss by Rewriting
梗概：関数型言語により定義できる関数の多くは停止性を持つ項書き換えシステムとして表現することができる．現在まで多項式解釈，行列解釈，リダクション順序など項書き換えシステムの停止性を証明する方法が知られている．こうした停止性の証明により，しばしば停止性だけでなく時間計算量と深く関係する書き換え回数の上限を求めることができる．本講演では経路順序と呼ばれるリダクション順序による計算量解析法についてM. Avanzini, G. Moser (共に University of Innsbruck)との共同研究の成果を報告する．さらに新しく導入する経路順序は多項式時間計算量に対して完全となることを説明する．
14:40-15:00 休憩20分
15:00-15:30
河野友亮（東京工業大学情報理工学研究科）
題目：論理CDの補完定理について
梗概：中間論理のひとつであるCD において、クレイグの補間定理が成り立たないことが[1]によって証明された。そのおおまかな内容の解説に加え、CDを少し変えた論理でもクレイグの補間定理が成り立たないことが[1]と同様の手法で証明できることを示す。
[1] Failure of interpolation in the intuitionistic logic of
constant domains, Grigori Mints, Grigory Olkhovikov,
Alasdair Urquhart
15:35-16:05
岩波克（東京工業大学情報理工学研究科）
題目：様相Lukasiewicz論理の公理化について
梗概：Lukasiewicz論理の様相論理化にはいくつかの流儀が知られているが、最も自然と思われる、Kripke modelを用いて様相論理化したものの公理について考える。
16:05-16:25 休憩20分
16:25-16:55
龍田真（国立情報学研究所）
題目：Non-Commutative First-Order Sequent Calculus
梗概：非可換一階シーケント計算NCLKについて講演する。まず、非可換positive fragment を普通の一階シーケント計算で前件にグループがあり右交換規則のない論理体系LK-に拡張する。次のことを示す。(1) NCLK は LJ に同等、(2) NCLKに交換規則を追加するとLKに同等になる、(3) LK-はLJに同等、(4) LK-とNCLKの間の翻訳。
17:00-17:30
龍田真（国立情報学研究所）
題目：TLCA未解決問題20番: 遺伝的置換子の型
梗概：TLCA未解決問題20番とは遺伝的置換子を特徴付ける型システムを見つけよという問題である．本講演はこれに答える．まず，遺伝的置換子全体が枚挙不可能であることを示すことにより，そのような型システムが存在しないことを証明する．次に，最善解として，可算無限個の型を与え，項がそのすべての型をもつこととその項が遺伝的置換子であることが同等であることを証明する．本講演はLICS2008と同じ内容である。
17:30-17:45
ビジネスミーティング（次回開催について）
18:00-20:00
懇親会
9/16（日曜日）
10:00-11:00
丸山善宏（Oxford University）
題目：Duality, Quantum Symmetry and Categorical Logic
梗概：After an introduction to duality theory, this talk is
two-fold while duality works as a unifying theme. In the
first part, we aim at articulating Chu Duality hidden in
Categorical Quantum Mechanics (i.e., dagger-compact
categories), thereby giving coalgebraic and logical
characterizations of quantum symmetries. In the second part,
we develop the framework of Categorical Universal Logic
building upon Lawvere's idea of hyperdoctrine, in which
duality theory can be exploited to find various models of
logic and set theory. From this perspective, we discuss the
following issues: Lawvere-Tierney topology; the tripos-topos
construction; and categorical quantum logic.
11:10-12:10
蓮尾一郎（東京大学情報理工学研究科）
題目：Nonstandard Static Analysis: Discrete Verification
Methodologies Transferred to Hybrid Applications
梗概：*Hybrid systems* are those which exhibit both discrete
"jump" and continuous "flow" dynamics. Their importance---as
components of *cyber-physical systems*---is paramount now
that more and more physical systems (cars, airplanes, etc.)
are controlled with computers.
There are naturally two directions towards the study of hybrid systems: *control theory* (typically continuous) and *formal verification* (typically discrete). For us from the formal verification community, therefore, the big challenge is how to incorporate continuous "flow" dynamics. Many existing techniques---such as hybrid automaton or Platzer’s differential dynamic logic---include differential equations explicitly. This incurs a difficult (and very interesting) question of how to handle differential equations.
In our project we take a different path of *turning flow into jump*---more precisely into infinitely many jumps each of which is infinitesimal (i.e. infinitely small). This makes everything discrete jump dynamics, to which all the discrete techniques accumulated in the community of formal verification readily apply. This venture is mathematically supported by *nonstandard analysis*, where we can rigorously speak about infinites and infinitesimals.
In the talk I will lay out: 1) our framework of a while-language and a Hoare-style program logic, augmented with an infinitesimal constant, for modeling and verification of hybrid systems; 2) how discrete verification techniques can be *transferred*, as they are, to hybrid applications, via the celebrated *transfer principle* in nonstandard analysis; and 3) the overview of our prototype automatic prover.
The talk is based on the joint work with Kohei Suenaga,
Kyoto University. References:
[1] Kohei Suenaga and Ichiro Hasuo. Programming with
Infinitesimals: A While-Language for Hybrid System
Modeling. Proc. ICALP 2011, Track B. LNCS 6756,
p. 392-403. Springer-Verlag.
[2] Ichiro Hasuo and Kohei Suenaga. Exercises in Nonstandard
Static Analysis of Hybrid Systems. To appear in Proc. CAV
2012.
12:10-13:30 昼食
13:30-14:15
Michele Basaldella (JAIST) （この講演は英語で行われます）
演題：An interactive semantics for classical arithmetic
梗概：In this talk, we introduce a sequent calculus which is
a variant of some well-known proof-systems introduced by
Novikoff, Tait, Coquand, and Herbelin. A common - and
perhaps the most interesting - aspect of these kinds of
calculi is that they can be used to provide a simple and
elegant formulation of syntactical derivability for first
order classical arithmetic... at a reasonable price: we have
to consider infinitary formulas and infinitary derivations,
rather than the usual finitary ones. In more detail, we
will talk about a calculus which has the following features:
* we derive sequents (finite multisets) of infinitary
propositional formulas, * some inference rules may have an
infinite number of premises, * derivations are infinitary
trees made of sequents. We also require that both formulas
and derivations are (infinitary) well-founded objects, which
means that both formulas and derivations can be defined
inductively. The main purpose of this talk is to define an
interactive semantics for derivations strongly inspired by
Girard's ludics. The target of this analysis is not the
derivability predicate 'the formula A is derivable' as
traditionally in logic, but the more subtle - and deeper -
statement 'p is a proof of the formula A'. Specifically, we
define a notion of untyped derivation and a procedure of
interaction (a kind of cut-elimination procedure) between
these untyped objects. Next, we we define two relations
'PROVES' and 'INTERACTIVELY' between untyped derivations 'p'
and formulas 'A' such that * 'p PROVES A' is defined
inductively, it corresponds to 'p is a proof of the formula
A' in the sequent calculus. * 'p INTERACTIVELY A' holds
whenever the interaction between 'p' and all the tests for
'A' (special derivations associated to 'A' ) terminates. We
finally show a soundeness-and-completeness theorem: 'p
PROVES A' if and only if 'p INTERACTIVELY A'.
14:15-15:00
木原貴行(JAIST)
題目：On some variants of the Jayne-Rogers THeorem via the
Posner-Robinson Join THeorem
梗概：位相空間上の関数 F が (m,n)-可測であるとは，ボレル階層の第 m 段階に属す集合の F による逆像が常にボレル階層の第 n 段階に属すことである．20世紀初頭，ルージンは任意のボレル可測関数は可算個の連続関数に分解可能か，すなわち可算的連続かどうか尋ねた．ルージン問題は1930年代に否定的解決が与えられ，現在では，m が n 未満ならば，可算的連続でない (m,n)-可測関数が存在することが知られている．その一方，Jayne-Rogers (1984) は，(2,2)-可測性と区分的連続性が同値であることを示した．Jayne-Rogers の定理の(n,n)-可測性への拡張，乃至，ボレル可測関数の階層における可算的連続性の境界の発見は，現代の実解析学における重要な問題の一つである．本発表では，連続的(n,n)-可測性の概念を定義し，チューリング次数の代数的構造に関する Posner-Robinson Join Theorem (1981) を介して，次の 5条件の同値性を与える：「連続的 (n+1,n+1)-可測」「連続的(2,n+1)-可測かつ可算的連続」「離散ベール第 n 類」「 n 世代神託学習によって同定可能」「第 n 階区分的連続」
15:05-15:35
宮部賢志（京都大学数理解析研究所）
題目：ゲーム論的確率論入門
梗概：ゲーム論的確率論では測度を使わずに確率の理論を展開する．その手法はランダムネスの理論に強く影響を受けており，証明では多くの場面でアルゴリズムを作ることが要求される．そこで何らかの形でコンピュータ科学にも参考になることを期待して，ゲーム論的確率論の基本的な考え方を解説する．
15:35-15:55 休憩20分
15:55-16:40
松尾亮太（名古屋大学大学院情報科学研究科計算機数理科学専攻）
題目：戦略的論理式
梗概：戦略の定義を、Strategic formulaによって表現されるよう
な写像のことと改めることによって、自然な戦略の理論の構築を目指す。R_G,n という命題論理の言語を定め、ここの論理式の内で戦略を表現するようなものをStarategic formula と呼ぶ。この枠組みによって、人が事実上用いることができる戦略の定義や、戦略の複雑さの妥当な定義が可能となる。我々の方法の応用として、ゲーム理論における最も有名な定理の一つであり、哲学的な問題点も併せ持った、The perfect folk theorem の解析を試みる。
16:45-17:45
佐藤雅大（名古屋大学多元数理科学研究科）
題目：Coqによる集合論と数学の実装
梗概：今回は私がCoqを用いて直観主義的集合論に基づいた数学の理論を構築したことについて発表する。Coqで集合論を展開するという試みはたくさん存在するが、今回は「Coqで集合論を展開した」ということより「Coqで展開できた集合論の上でどのように数学が展開できたか」という点に焦点を置いて発表したい。
17:45-18:00
次回予定アナウンスおよび挨拶
変更履歴：
09/09: 座長の割り振りの都合で蓮尾一郎さん，丸山善宏さん，Michele Basaldellaさんの講演を入れ替えました。
09/09: 講演時間をとりあえず元に戻しました。当日短縮して頂いても構わないようにプログラムを組みました。
09/09: 懇親会を30分繰り上げました。
09/10: 小林聡さんの講演がキャンセルされ，佐藤雅大さんの講演が繰り上がりました。
09/11: 佐藤雅大さんの題目を追加しました。
09/11: 研究集会が行われる部屋の情報を追加しました。
09/12: 科研費に関する記述を追加しました。
09/15: 1日目の時間の誤りを修正しました。
09/16: SLACS2012は本日無事終了致しました。皆様どうもありがとうございます。来年の世話人は東京大学の蓮尾一郎さんです。どうぞよろしくお願い致します。