14:30 〜 15:30 | 依頼講演 |
講演キャンセル |
証明の長さに関する諸問題
[handout]
新井敏康 abstract: (形式的)証明の長さに関するふたつの話題を取り上げる. ひとつはある組合せ論的命題を短く命題論理の通常の体系で証明することであり, ふたつめは不動点を表す述語によって述語論理を拡張した際の述語論理に対する加速定理である. |
Arrowの不可能性定理と判断形成の不可能性定理
[PDF]
酒井拓史 abstract:1951年,K. J. Arrow は, 「3つ以上の選択肢に対する選好を複数の投票者が投票した場合, それらを民主的にひとつの選好に集約することができない」という不可能性定理を証明しました. また,2000年代に入って,F. Dietrich, P. Petit, C. List らによって, 「論理的に関連づけられた複数の命題の正否を複数の個人が言明した場合,それらを民主的かつ無矛盾に集約することはできない」 という判断形成の不可能性定理が証明され, さらにこれから Arrow の不可能性定理が導かれることが示されています. 本講演では,判断形成の不可能性定理の証明の概要と Arrow の不可能性定理への応用, および関連する話題を紹介します. |
|
15:30 〜 16:00 | 休憩 |
16:00 〜 18:00 | 研究発表 |
A Compact and Efficient SAT-encoding of Finite Domain CSP
[PDF]
Tomoya Tanjo, Naoyuki Tamura, and Mutsunori Banbara |
|
Answer-Set Programming as a New Approach to Event-Sequence Testing
[PDF]
Esra Erdem, Katsumi Inoue, Johannes Oetsch, Jörg Pührer, Hans Tompits, and Cemal Yılmaz |
|
19:00 〜 | 会食 |
10:00 〜 11:30 | 研究発表 |
値変更コスト付き動的CSPの定式化とその解法
[PDF]
[PPTX]
波多野大督,平山勝敏 |
|
Non-monotone Dualization via Monotone Dualization
[PDF]
[PPT]
Yoshitaka Yamamoto, Hedetomo Nabeshima, and Koji Iwanuma |
|
11:30 〜 13:00 | 昼食 |
13:00 〜 15:00 | 研究発表 |
GlueMiniSat2.2.5 - 学習節評価尺度 LBD とリスタート戦略の改善
[PDF]
鍋島英知 |
|
SOLタブロー法に基づくSATソルバーの試作
[PDF]
[PPTX]
鈴木健士郎,鍋島英知 |
|
Unixのfork機能に基づくSATソルバーの並列化
[PDF]
[PPTX]
明石裕子 |
|
15:00 〜 15:30 | 休憩 |
15:30 〜 17:30 | 研究発表 |
多角形詰込み問題のSAT符号化の試み
[PDF]
田村直之,広瀬慎 |
|
Comparison of SAT Solvers using Sugar on 2008 CSP Solver Competition Benchmarks
[PDF]
田村直之 |
|
SAT符号化を用いた釣合い型不完備ブロック計画の構成に向けて
[PDF]
松中春樹,丹生智也,番原睦則,田村直之 |
|
上田研究室の進捗報告
[PDF-yamane]
[PPTX-yamane]
[PPTX-xxj]
[PDF-ueda]
[PPTX-ueda]
上田和紀,山根裕二,徐暁雋 |
|
17:30 〜 18:00 | 今後の研究方針について |
19:00 〜 | 会食 |
10:00 〜 11:00 | 2010年度業績の取りまとめについて JSAI 2011 オーガナイズドセッションについて |
11:00 〜 11:30 | まとめ,閉会 |