理工学研究科Graduate School of Science and Engineering
PRI500X4（情報学基礎 / Principles of informatics 500）応用論理・数理言語学特論２Applied Logic and Mathematical Linguistics ２
金沢 誠Makoto KANAZAWA
授業コードなどClass code etc
| 学部・研究科Faculty/Graduate school | 理工学研究科Graduate School of Science and Engineering |
| 添付ファイル名Attached documents | |
| 年度Year | 2023 |
| 授業コードClass code | YC008 |
| 旧授業コードPrevious Class code | |
| 旧科目名Previous Class title | |
| 開講時期Term | 秋学期授業/Fall |
| 曜日・時限Day/Period | 木3/Thu.3 |
| 科目種別Class Type | |
| キャンパスCampus | 小金井 |
| 教室名称Classroom name | 各学部・研究科等の時間割等で確認 |
| 配当年次Grade | |
| 単位数Credit(s) | 2 |
| 備考（履修条件等）Notes | |
| 実務経験のある教員による授業科目Class taught by instructors with practical experience | |
| カテゴリーCategory | システム理工学専攻 |
すべて開くShow all
すべて閉じるHide All
Outline (in English)
(Course outline)
Learn the basics of mathematical logic, using Fitch's system of natural deduction.
(Learning objectives)
- Learn how to express various propositions in the language of first-order logic
- To formalize simple proofs as derivations in natural deduction
- To understand the proofs of the soundness and completeness theorems
(Learning activities outside classrooms)
- Biweekly homework assignments
(Grading criteria)
- Homework assignments (40%) and final take-home exam (60%)
授業で使用する言語Default language used in class
日本語 / Japanese
授業の概要と目的（何を学ぶか）Outline and objectives
Fitchスタイルの自然演繹の体系を使って，数理論理学の基本的事項を学ぶ．
到達目標Goal
・命題を1階述語言語の論理式の形に記号化できる
・簡単な証明を自然演繹の推論図として形式化できる
・健全性定理と完全性定理の証明を理解する
この授業を履修することで学部等のディプロマポリシーに示されたどの能力を習得することができるか（該当授業科目と学位授与方針に明示された学習成果との関連）Which item of the diploma policy will be obtained by taking this class?
ディプロマポリシーのうち、「DP1」「DP2」「DP3」に関連
授業で使用する言語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.)
なし / No
フィールドワーク（学外での実習等）の実施Fieldwork in class
なし / No
授業計画Schedule
授業形態/methods of teaching：対面/face to face
※各回の授業形態は予定です。教員の指示に従ってください。
1[対面/face to face]：論理式
論理式で用いる記号とその意味
2[対面/face to face]：命題の記号化
いろいろな命題の論理式による表現の仕方
3[対面/face to face]：形式的推論(1)
論理記号の導入規則と除去規則，等号に関する推論規則
4[対面/face to face]：形式的推論(2)
形式的証明の例
5[対面/face to face]：1階述語言語
等号を持つ1階の述語言語の定義
6[対面/face to face]：自然演繹
Fitchスタイルの自然演繹における推論図の厳密な定義
7[対面/face to face]：論理的同値性
互いに導出可能な論理式の性質
8[対面/face to face]：健全性定理と完全性定理
健全性定理の証明，完全性定理の証明のための補題
9[対面/face to face]：完全性定理
Henkin流の完全性定理の証明
10[対面/face to face]：演繹式計算
演繹式を用いた自然演繹の体系NK，NKとFitchスタイルの自然演繹の体系との対応
11[対面/face to face]：Gentzenの体系(1)
Gentzenの演繹式計算LK
12[対面/face to face]：Gentzenの体系(2)
LKとNKとの対応
13[対面/face to face]：Gentzenの基本定理
LKに関するGentzenの基本定理の証明
14[対面/face to face]：決定手続き
命題計算における証明可能性を判定するWangのアルゴリズム
授業時間外の学習（準備学習・復習・宿題等）Work to be done outside of class (preparation, etc.)
【本授業の準備・復習時間は、各4時間を標準とします。】授業中に示された演習問題を解く．講義ノートを読んで復習する．
テキスト（教科書）Textbooks
なし．適宜講義ノートを配布する．
参考書References
角田 譲『数理論理学入門』朝倉書店，1996年．
成績評価の方法と基準Grading criteria
宿題(40%)と期末レポート課題(60%)による．
学生の意見等からの気づきChanges following student comments
特になし．