[logic-ml] SLACS 2011 のご案内および講演募集 （再々送）

[Kamo Hiroyasu]

logic-mlのみなさま
（重複をご容赦ください）
SLACS 2011 の世話人をおおせつかっている奈良女子大学の鴨です。

2日前になりました。暫定プログラム（ほぼ最終版）をお送りします。講演の追
加があれば、（予備）と書かれている時間に割り当てます。それ以外は、この
まま最終版となる見込みです。
--
SLACS 2011 - 記号論理と情報科学研究集会

開催要項

開催日：2011年9月12日(月)午後 〜 9月13日(火)午後
場所：奈良女子大学G棟G302教室
  奈良女子大学へは、大阪または京都から近鉄が便利です。近鉄奈良駅から徒歩約5分です。
  当日は夏期休暇中で南門が閉鎖されているため、正門におまわりください。
	アクセスマップ http://www.nara-wu.ac.jp/accessmap.html
	キャンパスマップ http://www.nara-wu.ac.jp/image_c/campusmap2.jpg
懇親会：9月12日夜に懇親会を予定しています．
  一般5000円程度、学生割引ありで調整中です。

参加費，参加申込はともに不要です．（懇親会につきましては費用を御負担いただきます．）


暫定プログラム（ほぼ最終版）
(2011年9月10日19:10現在)

9月12日(月)

14:00--14:10 （オープニング、連絡など）

14:10--14:30 小島侑子（奈良女子大学）「小型ロボットを制御するための汎用ライブラリの開発」
    近年、安価で小型なロボットの登場がロボットの研究に新たな可能性をも
    たらしている。我々は、その1つであるLEGO MINDSTORMS NXTの制御プログ
    ラムの作成を容易にするため、新たなNXT制御ライブラリを提案する。特に、
    反射的行動を記述したライブラリにするなど、ロボットの行動制御の研究
    を容易にすることを主眼に置く。

14:30--15:00 中澤巧爾（京都大学）「Combinators for streams」
    本発表では，型無しラムダ・ミュー計算に同等なcombinatory calculusと
    してCL^\muを提案する． また，型無しラムダ・ミュー計算のモデルとして
    stream modelを定義し，CL^\muの構造をもとにして stream modelの代数的な
    特徴付けを行なう．

（休憩）

15:45--16:30	Michele Basaldella（京都大学）「Infinitary completeness in ludics」
    Traditional Goedel completeness holds between finite proofs and
    infinite models over formulas of finite depth. In this talk, we
    generalize it to a completeness theorem between infinite proofs
    and infinite models over formulas of infinite depth (that include
    recursive types).

16:30--17:00	藤田恵（奈良女子大学）「実世界の多様性に適応したBDIロボットについて」
    近年、単一の目標達成に特化されたロボットでなく、動的に変化する環境
    のもとで自らの目的を達成するよう動作するロボットの実現が重要な研究
    課題となってきている。我々は、BDIモデルを実装したBDIロボットによる
    ロボット制御が、複雑で多様性に富んだ実世界において自らの目的を実現
    していくロボットのためのアーキテクチャとして有効であることを示す。
    特に、意図の保持と破棄という機構によって、目標を達成する手段を柔軟
    に切り替えたり、複数の目的を並行に保持し整合的に実行したりできる
    BDIモデルの能力が、多様性への適応に非常に有用であることを論じ、また、
    実験を通じてそれを示す。

17:00--17:30 （予備）

（移動）

18:30-- 懇親会

9月13日(火)

9:45--10:15	（予備）

10:15--10:45	岡章弘（京都産業大学）・三好博之（京都産業大学）「リアクティブシステムのモノイダル2-圏による定式化」
    LeiferとMilnerは圏を用いて抽象的なリアクティブシステムを定式化し，
    Milnerはその枠組みで具体的にバイグラフを用いてシステムの記述を行う
    研究を行った。しかしMilnerの体系では，リアクティブシステムからラベ
    ル付き遷移系(LTS)を導くのにサポートと呼ばれるデータが必要であり，そ
    のために圏ではなく前圏(precategory)を用いているためかなり複雑である。
    そこでSosanneとSoboci\'nskiはサポートと2-圏の2-セルとの類似性に着目
    して亜群によりenrichされた2-圏による定式化を行った。本講演ではこれ
    にモノイダル積を加えることによりシステムの並置を陽に含む定式化を行
    う。これによりシステムをより自然に圏論的な構成として記述することが
    できる。ここではさらにstcasticなシステムへの圏論的な拡張も視野に入
    れている。

（休憩）

11:15--12:00	向井国昭（慶應義塾大学）「チャネル理論の分類概念再訪」
    Barwise/Seligmanのチャネル理論(1997)は，タイプとトークンの間の関係
    としての分類だけでなく，タイプ間の制約としての局所論理を動員して情
    報の流れをモデル化しようとする試みである．チャネル理論は，すでに抽
    象設計論(角田・菊池) など多くの発展および応用を得ている．

    チャネル理論の局所論理は，大域カット則を充足する理論を正則とする．
    なぜ大域カットなのだろうか？ また，大域カットは通常のカット推論規則
    よりも強いが，有限の証明図および有限のシーケントに限定すればそれら
    は等価となるのだろうか？

    この「保守拡大性」に関しては，選択公理を使って肯定的な証明が得られ
    た．このようにチャネル理論の「重箱の隅」をつついているうちに，分類
    と情報射の意味と役割が次第によくわかってきた．大域カットのねらいも
    見えてきた．さらに位相空間(連続写像)や可測空間(可測写像)，もっと身
    近な線形空間(線形写像)やオートマトン(模倣)など， おなじみの数学的構
    造がすべてチャネル理論の分類(情報射)であることが実感をもって確認で
    きた．この実感の共有は情報をめざす多くの人とくに学生諸君にとっても
    有用であると信じる．なお，井出陽子氏の関連結果 (修士論文2011) にも
    ふれる．

12:00--12:20	片山寛子（奈良女子大学）「BDIロジックに基づくエージェント実行系の構築に向けて」
    BDIモデルは、合理的エージェントの実現の基盤としてよく知られているが、
    BDIモデルの論理的な形式化に用いられるBDIロジックと現在提案されてい
    る手続的なBDIエージェントの実行系との間にはギャップがあることが指摘
    されている。本論文では、BDIロジックでの論理式による記述をそのまま実
    行可能なプログラムとして扱うようなBDIエージェントの実行系の実現に関
    するアイデアについて述べる。

（休憩）

13:20--14:20	丸山善宏（京都大学）「Duality and Abramsky's Representation of Quantum Systems」
    Samson Abramsky recently proposed to represent quantum systems (or
    physical systems in general) as Chu spaces and as coalgebras. In
    this talk, we analyze duality-theoretic consequences of his
    representation of quantum systems, and then place the resulting
    dualities in a wider context of general duality theory, with the
    ultimate aim of clarifying the nature of duality between states
    and observables in quantum physics. We finally touch upon
    philosophical issues relating Abramsky's representation to Karl
    Popper's notion of verisimilitude.

14:20--14:50	小川美樹（奈良女子大学）「汎用的な証明図作成支援ソフトの構築」
    証明図作成支援ソフトをJAVAで構築する。既存の物と比較して、次のよう
    な長所を持つものを作成しようと考えている。まず、JAVAで構築すること
    によって汎用性の高いものにする。また、柔軟にレイアウトする機能を加
    える。さらに、半自動証明の機能も加える。

14:50--15:50 （予備）

15:50--16:00	（クロージング、次回予告など）