理工学部Faculty of Science and Engineering
MAT300XG（数学 / Mathematics 300）論理と推論Automated Inference
金沢 誠Makoto KANAZAWA
授業コードなどClass code etc
| 学部・研究科Faculty/Graduate school | 理工学部Faculty of Science and Engineering |
| 添付ファイル名Attached documents | |
| 年度Year | 2023 |
| 授業コードClass code | H9100 |
| 旧授業コードPrevious Class code | |
| 旧科目名Previous Class title | |
| 開講時期Term | 春学期授業/Spring |
| 曜日・時限Day/Period | 木3/Thu.3 |
| 科目種別Class Type | |
| キャンパスCampus | 小金井 |
| 教室名称Classroom name | 小西館‐W303 |
| 配当年次Grade | 3年 |
| 単位数Credit(s) | |
| 備考（履修条件等）Notes | |
| 他学部公開科目Open Program | |
| 他学部公開（履修条件等）Open Program (Notes) | |
| グローバル・オープン科目Global Open Program | |
| 成績優秀者の他学部科目履修制度対象Interdepartmental class taking system for Academic Achievers | |
| 成績優秀者の他学部科目履修（履修条件等）Interdepartmental class taking system for Academic Achievers (Notes) | |
| 実務経験のある教員による授業科目Class taught by instructors with practical experience | |
| SDGsCPSDGs CP | |
| アーバンデザインCPUrban Design CP | |
| ダイバーシティCPDiversity CP | |
| 未来教室CPLearning for the Future CP | |
| カーボンニュートラルCPCarbon Neutral CP | |
| 千代田コンソ単位互換提供（他大学向け）Chiyoda Campus Consortium | |
| カテゴリー＜理工学部＞Category |
創生科学科 学科専門科目 |
すべて開くShow all
すべて閉じるHide All
Outline (in English)
(Course outline)
The course introduces proof systems for propositional and first-order logic and how to use a proof assistant on a computer.
(Learning objectives)
The goal is to be able to write formal proofs of simple laws about sets and relations in a formal system called natural deduction. Students are expected to master both pencil-and-paper proofs and formalized proofs in a proof assistant.
(Learning activities outside of classroom)
Students are expected to read the relevant part of the textbook prior to each class meeting, and to work on the assigned homework.
(Grading Criteria)
The grade will be based on the submitted homework problems (100%).
授業で使用する言語Default language used in class
日本語 / Japanese
授業の概要と目的（何を学ぶか）Outline and objectives
記号論理の証明体系について学び，証明図の書き方を習得する．集合と関係に関する基本的な法則を証明体系の中で証明できるようになる．紙と鉛筆による証明と定理証明支援系を用いた計算機上での証明の両方に習熟する．
到達目標Goal
次に掲げる能力を身につける．
・命題論理と一階論理の形式言語による命題の記号化
・自然演繹の体系の推論規則の理解
・基本的な論理法則の形式的証明の構築
・集合と関係に関する基本的な法則の理解
・上記法則の形式的証明の構築
・形式的証明の証明支援系による表現の習得
この授業を履修することで学部等のディプロマポリシーに示されたどの能力を習得することができるか（該当授業科目と学位授与方針に明示された学習成果との関連）Which item of the diploma policy will be obtained by taking this class?
ディプロマポリシーのうち、「DP1」と「DP2」と「DP4」に関連
授業で使用する言語Default language used in class
日本語 / Japanese
授業の進め方と方法Method(s)（学期の途中で変更になる場合には、別途提示します。 /If the Method(s) is changed, we will announce the details of any changes. ）
毎回次のような構成で講義と演習を組み合わせて進める．
・前回に課された課題の解説
・テキストの該当箇所に関する講義
・演習問題の提示
・演習問題の解説
・課題の提示
課題等の提出・フィードバックは「学習支援システム」を通じて行う．
アクティブラーニング（グループディスカッション、ディベート等）の実施Active learning in class (Group discussion, Debate.etc.)
あり / Yes
フィールドワーク（学外での実習等）の実施Fieldwork in class
なし / No
授業計画Schedule
授業形態/methods of teaching：対面/face to face
※各回の授業形態は予定です。教員の指示に従ってください。
1[対面/face to face]：導入，命題論理
数学的証明の例，論理記号，命題論理の推論規則
2[対面/face to face]：命題論理の自然演繹の体系
命題論理の自然演繹の証明図の構築の演習
3[対面/face to face]：証明支援系による命題論理
Leanによる命題論理の自然演繹の証明の書き方の演習
4[対面/face to face]：古典論理
背理法を用いた証明とそのLeanによる書き方
5[対面/face to face]：命題論理の意味論
真理値割り当て，真理表，反例の構成
6[対面/face to face]：一階論理
一階論理の言語，等号，一階論理による命題の表現
7[対面/face to face]：一階論理の自然演繹の体系
一階論理の推論規則，等号に関する規則，証明図の構築の演習
8[対面/face to face]：証明支援系による一階論理
Leanによる一階論理の自然演繹の証明の書き方の演習，等式の連鎖による証明
9[対面/face to face]：一階論理の意味論
一階論理の言語に対するモデル，モデルにおける真理，恒真性と論理的帰結の概念
10[対面/face to face]：集合
集合の記法，集合に関する演算と法則，添字付き集合族の和と共通部分，デカルト積，べき集合
11[対面/face to face]：証明支援系による集合の扱い
集合に関する法則の証明のLeanによる書き方の演習
12[対面/face to face]：関係
順序，同値関係，等号の性質
13[対面/face to face]：証明支援系による関係の扱い
関係に関する法則の証明のLeanによる書き方の演習
14[対面/face to face]：総合演習
集合と関係に関するLeanによる証明の演習
授業時間外の学習（準備学習・復習・宿題等）Work to be done outside of class (preparation, etc.)
【本授業の準備・復習等の授業時間外学習は、4時間を標準とする】
・事前にテキストの該当箇所を読む
・与えられた演習問題に取り組む
テキスト（教科書）Textbooks
Jeremy Avigad, Robert Y. Lewis, and Floris van Doorn. 2017. Logic and Proof. オンラインテキスト．
http://leanprover.github.io/logic_and_proof/index.html
参考書References
山田俊行．2018. はじめての数理論理学．森北出版．
成績評価の方法と基準Grading criteria
定期的に課す課題の成績による（100%）．
学生の意見等からの気づきChanges following student comments
本年度授業担当者変更によりフィードバックできません．
学生が準備すべき機器他Equipment student needs to prepare
ノートパソコン．