授業の目的 【日本語】
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 the 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 correctness and safty of comoputer software. |
|
|
授業の内容や構成
Course Content / Plan | | 論理学1において学んだ基礎論理学にもとづいて，コンピュータ科学における論理学の適用技法について解説する。とくに，（1）SATソルバなどを用いた充足可能性判定による問題解決，および（2）導出原理による証明に基づく論理型プログラミングの基礎について学ぶ。
1. 数学的準備
2. 命題論理式の充足可能性判定
3. SATソルバによる問題解決
4. 述語論理のシーケント計算による定理証明
5. エルブランの定理
6. 導出原理による定理証明
7. 論理型プログラミング基礎
8. 総括 | Based on Logic 1 lecture, this leture provides the application of the mathematical logic in computer science. We give the fundamental knowledge and techniques in (1) problem solving by satisifiablity checking using SAT solvers, and (2) proofs with the resolution principle and the foundations for the logic programming.
1. Mathematical preliminaries;
2. Satisfiablity checking in propositional logic;
3. Problem solving by SAT solvers;
4. Sequent calculus for predicate logic;
5. Herbrand Therorem;
6. Theorem proving by the resolution principle;
7. Foundations of the logic programming; and
8. Summary |
|
|
履修条件・関連する科目
Course Prerequisites and Related Courses | | |
|
成績評価の方法と基準
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 materical 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) | | |
|