学部・大学院区分
Undergraduate / Graduate		情報学部
時間割コード
Registration Code		1000093
科目区分
Course Category
専門基礎科目（コンピュータ科学科 対象）
科目名　【日本語】
Course Title		論理学２ｃ
科目名　【英語】
Course Title		Logic 2c
コースナンバリングコード
Course Numbering Code		SIS-03-2005-J
担当教員　【日本語】
Instructor		結縁 祥治 ○ 中澤 巧爾
担当教員　【英語】
Instructor		YUEN Shoji ○ NAKAZAWA Koji
単位数
Credits		1
開講期・開講時間帯
Term / Day / Period		秋２期 月曜日 ２時限
Fall2 Mon 2
対象学年
Year		２年
2
授業形態
Course style		講義
Lecture
開講系（学部）・開講専攻（大学院）
Subject
共通（CS）
必修・選択
Required / Selected
ＣＳ必修


授業の目的　【日本語】
Goals of the Course(JPN)
論理学1において学んだ基礎論理学にもとづいて，コンピュータ科学における論理学の適用技法について習得する。（1）SATソルバなどの制約解消系による充足可能性判定による問題解決，および，（2）導出原理による証明に基づく論理型プログラミングの基礎について講義を行う。
授業の目的　【英語】
Goals of the Course
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, and (2) the foundation of logic programming based on the refutation with the resolution principle.
到達目標　【日本語】
Objectives of the Course(JPN)
コンピュータ科学において理論・応用両面で重要な役割を果たす論理学の基礎とその適用技法について学ぶ。とくに，ソフトウェア科学において論理学のアイディアがどのように利用されているかを理解する。
到達目標　【英語】
Objectives of the Course
This lecture provides the basics of mathematical logic for computer science in theory and application. This lecture focuses on the topics of the foundations and techniques in terms of programming and verification useful for the correctness and safety of computer software.
授業の内容や構成
Course Content / Plan
論理学1において学んだ基礎論理学にもとづいて，コンピュータ科学における論理学の適用技法について解説する。とくに，（1）SATソルバなどを用いた充足可能性判定による問題解決，および（2）導出原理による証明に基づく論理型プログラミングの基礎について学ぶ。

1. 数学的準備
2. 命題論理式の充足可能性判定
3. SATソルバによる問題解決
4. エルブランの定理
5. 導出原理による定理証明
6. 論理型プログラミング
7. 総括
Based on the Logic 1 lecture, this lecture provides the application of mathematical logic in computer science. We give the fundamental knowledge and techniques in (1) problem solving by satisfiability checking using SAT solvers and (2) proofs with the resolution principle and the foundations for logic programming.
1. Mathematical preliminaries;
2. Satisfiability checking in propositional logic;
3. Problem solving by SAT solvers;
4. Herbrand Therorem;
5. Theorem proving by the resolution principle;
6. Logic programming; and
7. Summary
履修条件・関連する科目
Course Prerequisites and Related Courses
論理学１
Logic 1
成績評価の方法と基準
Course Evaluation Method and Criteria
講義中に与える演習課題の評価50％，期末試験50％．合計100点満点で60点以上を合格とする。
50% by the exercises given in the lectures and 50% by the term-end examination.
教科書・参考書
Textbook/Reference book
必要に応じて資料を配布する。
We provide the necessary materials in the lectures.
課外学習等（授業時間外学習の指示）
Study Load(Self-directed Learning Outside Course Hours)
講義において説明した内容を理解するために課題を与える。
We require to submit brief exercises.
授業開講形態等
Lecture format, etc.
対面による講義を基本とするが，状況に応じて決定する。期末試験が対面で実施できない場合は、レポートによる評価を行う。
遠隔授業（オンデマンド型）で行う場合の追加措置
Additional measures for remote class (on-demand class)