━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ 数理論理学 学習事項 ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
受講にあたって必要な復習事項を示す. また,本講義で扱う学習事項を教科書の節番号と共に示す. ●復習しておくこと ・集合論 (集合,関係,順序,写像) の基本的な定義 ・C言語プログラムの基本的な読み書き ・帰納的 (再帰的) 定義の方法 ●数理論理学の基礎 授業概要の説明 数理論理学の導入 *第1回 ・数理論理学の目的 (序章) ・形式化 (序章, 1-1) ●論理式と証明法 数学的主張の記号表現 数学の基本的な証明法(論理式の構造に沿った系統的な証明) *第2回 ・命題と述語 (1-1) ・論理結合子(¬,∨,∧,⇒,⇔) (1-2) ・論理式 (1-2) ・真理表 (1-2) *第3回 ・論理式の真偽 (1-2) ・証明法:含意の直接証明 (2-1) ・含意の意味 (1-4) *第4回 ・証明法:含意の間接証明(対偶と背理法) (2-1) ・証明法:同値の証明(双方向の含意) (2-2) ・証明法:同値の証明(同値変形) (2-2) *第5回 ・量化子(∀,∃) (1-3) ・全称と存在 の基本表現 (1-3, 1-4) ・述語と集合 の対応 (1-4) *第6回 ・よく使う論理表現 (1-5) ・全称と存在 の否定 (1-7) *第7回 ・証明法:全称と存在 の証明 (2-3) ・証明法:論理法則の利用 (2-4) ・否定を使った言い換え (1-7) *第8回 ・証明法:否定の証明 と 反証 (2-4) ・集合と論理 (1-6) ・全称と存在 の併用 (1-8) ●自然演繹 記号操作で証明を進める論理の枠組み 自然演繹の形式体系 *第9回 ・自然演繹の基礎 (序章,3-1) ・帰納的定義 (なし) *第10回 ・述語論理の構文論 (3-9) ・証明の形式化 (1-1, 3-9) ・命題論理の自然演繹 (3-2) *第11回 ・命題論理の自然演繹 (3-3, 3-4) *第12回 ・述語を扱う準備 (3-6) ・述語論理の自然演繹 (3-6, 3-7) *第13回 ・関数記号を使う自然演繹 (3-8) ・背理法を使う自然演繹 (3-5) ●述語論理の意味論 主張や推論の正しさを数学的に厳密に議論 *第14回 ・形式体系の健全性と完全性 (3-10) ・構造による言語の意味付け (3-10) *第15回 ・恒真性と充足可能性 (3-10) ●応用 数理論理学の応用 *第15回 (時間があれば) ・論理による問題解決 ・充足可能性判定 (SATソルバー) ・論理型プログラミング言語 ・証明支援システム ・定理自動証明器 ・ソフトウェアの正当性検証 ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ 授業のホームページ 山田 俊行 https://www.cs.info.mie-u.ac.jp/~toshi/