数理論理学特論

• 神戸大学 田村直之 tamura@kobe-u.ac.jp

• 2019-08-19 Mon– 2019-08-22 Thu
  • 2限: 10:40–12:10 (月曜日は3限開始)
  • 3限: 13:00–14:30
  • 4限: 14:40–16:10
  • 5限: 16:20–17:50

イントロ

• 講義: イントロ (PDF)
• 講義: 組合せ爆発と計算 (PDF)
• 講義: 制約プログラミングとSATソルバー
• 講義: Knuth先生の『TAOCP 7.2.2.2 Satisfiability』を読む
  • http://bach.istc.kobe-u.ac.jp/lect/taocp-sat/docs/
• 演習: Google Colaboratory の利用

• 講義: Knuth先生の『TAOCP 7.2.2.2 Satisfiability』を読む
  • 充足可能性
  • 単純な例 (ファン・デル・ベルデン数)

• 講義: Knuth先生の『TAOCP 7.2.2.2 Satisfiability』を読む
  • 厳密被覆問題 (Langford対)
  • グラフ彩色問題

SATソルバーの応用

• 有限オートマトン
  • http://bach.istc.kobe-u.ac.jp/lect/tfpl/tfpl-nfa.html
• イラストロジック

その他の候補

• 経路探索問題 (ナンバーリンク)
• デジタル断層撮影
• 美術館パズル
• 推理パズル
• 故障検査
• 有界モデル検査

1. 命題論理
2. 命題論理の推論体系 (融合原理)
3. SATソルバーの基礎 (PDF)
4. 高速SATソルバーの原理 (PDF)
5. SATソルバーは問題解決のための「銀の弾丸」か? (PDF)
6. パズルをSugar制約ソルバーで解く (PDF)
7. 組合せ爆発と計算 (PDF)
8. 制約プログラミング入門 (PDF)
9. 制約最適化問題とSAT符号化 (PDF)
10. SATとシステム検証 (PDF)
11. Prolog入門 (PDF)
12. Prolog Cafe (PDF)
13. 数理論理学入門 (PDF)
14. 述語論理式による記述の練習 (PDF)