学部・大学院区分情報学部
時間割コード1000093
科目区分
専門基礎科目（コンピュータ科学科 対象）
科目名　【日本語】論理学２ｃ
科目名　【英語】Logic 2c
コースナンバリングコード
担当教員　【日本語】結縁　祥治 ○ 中澤　巧爾
担当教員　【英語】YUEN Shoji ○ NAKAZAWA Koji
単位数1
開講期・開講時間帯秋２期 金曜日 ２時限
Fall2 Fri 2
対象学年２年
2
授業形態講義
Lecture
開講系（学部）・開講専攻（大学院）
共通（CS）
必修・選択
ＣＳ必修


授業の目的　【日本語】
論理学1において学んだ基礎論理学にもとづいて，コンピュータ科学における論理学の適用技法について習得する。（1）SATソルバなどの制約解消系による充足可能性判定による問題解決，（2）導出原理による証明に基づく論理型プログラミングの基礎，および（3）ホーア論理に代表されるプログラム論理によるプログラムの検証について講義を行う。
授業の目的　【英語】
Based on the fundamental knowledge of logic in Logic 1, this course introduces the applications of logic in computer science for the following topics. (1) Problem solving by satisfiability of formulae using constraint solvers such as the SAT solver, (2) the foundation of logic programming based on the refutation with the resolution principle, and (3) the verification technique of programs using Hoare logic.
到達目標　【日本語】
コンピュータ科学において理論・応用両面で重要な役割を果たす論理学の基礎とその適用技法について学ぶ。とくに，ソフトウェア科学において論理学のアイディアがどのように利用されているかを理解する。
到達目標　【英語】
授業の内容や構成
論理学1において学んだ基礎論理学にもとづいて，コンピュータ科学における論理学の適用技法について解説する。とくに，（1）ホーア論理に代表されるプログラム論理によるプログラム検証，（2）SATソルバなどを用いた充足可能性判定による問題解決，および（3）導出原理による証明に基づく論理型プログラミングの基礎について学ぶ。

1. 数学的準備
2. プログラミング言語の公理的意味論
3. 定理証明器
4. 命題論理式の充足可能性判定
5. SATソルバによる問題解決
6. エルブランの定理
7. 導出原理と論理型プログラミング
8. 総括
履修条件・関連する科目
成績評価の方法と基準
講義中に与える演習課題の評価50％，期末試験50％．合計100点満点で60点以上を合格とする。
教科書・参考書
必要に応じて資料を配布する。
課外学習等（授業時間外学習の指示）
講義において説明した理論を理解するために課題を与える。
授業開講形態等
遠隔授業（オンデマンド型）で行う場合の追加措置