知的情報処理特論のシラバス情報
| 科目名称 Course title(Japanese) |
知的情報処理特論 | 科目番号 Course number |
14MAAPM512 | |
|---|---|---|---|---|
| 科目名称（英語） Course title(English) |
Advanced intelligent information process | |||
| 授業名称 Class name |
知的情報処理特論 | |||
| 教員名 | 松崎 拓也 |
|---|---|
| Instructor | Takuya Matsuzaki |
| 開講年度学期 | 2022年度 前期 |
|---|---|
| Year/Semester | 2nd semester |
| 曜日時限 | 水曜2限 |
|---|---|
| Class hours | Tuesday, 2nd period |
| 開講学科 Department |
理学研究科 応用数学専攻 Graduate School of Science, Department of Applied Mathematics |
|---|---|
| 外国語のみの科目 （使用言語） Course in only foreign languages (languages) |
- |
| 単位 Course credit |
2.0 | 授業の主な実施形態 Main class format |
対面型講義/classroom lecture |
|---|
| 概要 Descriptions |
命題論理と一階述語論理の基礎について学習したのち，種々の決定手続き（Decision Procedure）について学習する．この講義で学習する決定手続きとは，論理式で記述された命題の成立・不成立を決定するアルゴリズムのことである．決定手続きは，人工知能（自動推論）と数式処理の中間的な研究領域であり，ソフトウェア検証，プログラム合成，自動定理証明などへの応用がある． We first learn basics of propositional and first-order predicate logic, and then learn various decision procedures. Decision procedures are algorithms to derive an answer (yes/no) to a proposition expressed in a logic formula. It is a research area in the intersection of artificial intelligence (automated reasoning) and computer algebra and has applications to software verification, program synthesis, automated theorem proving, etc. |
|---|---|
| 目的 Objectives |
論理学の基礎および決定手続きについて習得する． この科目は、本専攻のカリキュラム・ポリシーに定める「統計科学・計算数学・情報数理の3部門を設け、いずれか一つを主研究部門とする一方で、3部門を横断的に学習・研究することができる」ことを実現するための科目です。また、本専攻のディプロマ・ポリシーに定める「応用数学の分野において高度な専門的学識と研究能力を持つことで、論理的・批判的に思考し、専門分野及び関連分野の諸問題を能動的に解決することができる能力」を養うための科目です。 To learn the basics of formal logic and decision procedure. |
| 到達目標 Outcomes |
命題論理と一階述語論理の Syntax と Semantics および完全性について理解し，説明できる． 種々の決定手続きについて理解し，説明できる． To understand the syntax and semantics of propositional and first-order predicate logic. To understand various decision procedures. |
| 履修上の注意 Course notes prerequisites |
各回の講義後に十分な復習を行うこと． また毎回， 演習問題を解いて提出すること． The participants are supposed to review each lecture and solve practice problems. |
| アクティブ・ラーニング科目 Teaching type（Active Learning） |
|||
|---|---|---|---|
| 課題に対する作文 Essay |
○ | 小テストの実施 Quiz type test |
- |
| ディベート・ディスカッション Debate/Discussion |
- | グループワーク Group work |
- |
| プレゼンテーション Presentation |
- | 反転授業 Flipped classroom |
- |
| その他（自由記述） Other（Describe） |
- | ||
| 準備学習・復習 Preparation and review |
各回の講義後に十分な復習を行うこと． また毎回， 演習問題を解いて提出すること． The participants are supposed to review each lecture and solve practice problems. |
|---|---|
| 成績評価方法 Performance grading policy |
レポート課題による． Reports. |
| 学修成果の評価 Evaluation of academic achievement |
・S：到達目標を十分に達成し、極めて優秀な成果を収めている ・A：到達目標を十分に達成している ・B：到達目標を達成している ・C：到達目標を最低限達成している ・D：到達目標を達成していない ・-：学修成果の評価を判断する要件を欠格している ・S：Achieved outcomes, excellent result ・A：Achieved outcomes, good result ・B：Achieved outcomes ・C：Minimally achieved outcomes ・D：Did not achieve outcomes ・-：Failed to meet even the minimal requirements for evaluation |
| 教科書 Textbooks/Readings |
・教科書を使用する場合は、MyKiTS(教科書販売サイト)から検索・購入可能ですので以下のURLにアクセスしてください。 https://gomykits.kinokuniya.co.jp/tokyorika/ ・Search and purchase the necessary textbooks from MyKiTS (textbook sales site) with the link below. https://gomykits.kinokuniya.co.jp/tokyorika/ |
| 参考書・その他資料 Reference and other materials |
前半は 小野寛晰 「情報科学における論理」 日本評論社 を教科書とする． 後半は Daniel Kroening & Ofer Strichman. "Decision Procedures (Second edition)” Springer. を教科書とする． “Decision Procedure (Second edition)” は学校図書館からPDFファイルがダウンロードできる． リンク： http://search.ebscohost.com/login.aspx?direct=true&db=edspub&AN=edp12102819&lang=ja&site=eds-live |
| 授業計画 Class plan |
前半 1. 命題論理の Syntax と Semantics 2. 命題論理の証明手続き 3. 命題論理の完全性 4. 一階述語論理の Syntax と Semantics 5. 一階述語論理の証明手続き ６. 一階述語論理の完全性 後半 7. 命題論理の決定手続き（１） 8. 命題論理の決定手続き（2） 9. DPLL(T) 10. 等号論理と uninterpreted function 11. 線形算術(1) 12. 線形算術(2) 13. ビットベクトル 14. 配列 15. ポインタ論理 Part 1 1. Syntax and semantics of propositional logic 2. Proof in propositional logic 3. Completeness of propositional logic 4. Syntax and semantics of first-order predicate logic 5. Proof in first-order predicate logic 6. Completeness of first-order predicate logic Part 2 7. Decision procedures for propositional logic (1) 8. Decision procedures for propositional logic (2) 9. DPLL(T) 10. Equalities and uninterpreted functions 11. Linear arithmetic (1) 12. Linear arithmetic (2) 13. Bit vectors 14. Arrays 15. Pointer logic |
|---|
| 教職課程 Teacher-training course |
|
|---|---|
| 実務経験 Practical experience |
- |
| 教育用ソフトウェア Educational software |
- |
| 備考 Remarks |
|---|
| 991JB07 |
