シラバスの詳細な内容を表示します。
→ 閉じる（シラバスの一覧にもどる）
| 開講年度 | 2018 年度 | |
|---|---|---|
| 開講区分 | 工学部情報工学科 ・基礎教育 | |
| 受講対象学生 |
学部(学士課程) : 2年次 |
|
| 選択・必修 | 必修 学科必修 |
|
| 授業科目名 | 数理論理学 | |
| すうりろんりがく | ||
| Mathematical Logic | ||
| 単位数 | 2 単位 | |
| 他学部・他研究科からの受講 |
|
|
| 市民開放授業 | 市民開放授業ではない | |
| 開講学期 |
後期 |
|
| 開講時間 |
金曜日 3, 4時限 |
|
| 開講場所 | 工学部指定教室 | |
| 担当教員 | 山田俊行（工学部情報工学科） | |
| YAMADA, Toshiyuki | ||
| 授業の概要 | 数理論理学は，数学的な主張を厳密に表現したり，系統的な証明方針に沿って論証を進めるための基礎となる．情報工学の分野でも，アルゴリズム理論やプログラム意味論を展開する道具として，また，論理プログラミングやソフトウェア解析・検証などの基礎技術として，広く使われている．この講義の目的は，数理論理学の基礎と応用について理解を深めることである．まず，命題論理や述語論理の構文，意味，証明，導出原理などの基本事項について学ぶ．さらに，論理プログラミングや計算機による定理証明技術などの工学的な応用について触れる機会をもつ． |
|---|---|
| 学習の目的 | 数理論理学の基礎と応用について，次の観点から理解を深める． ・命題論理や述語論理の 構文・証明・意味・導出原理 ・論理プログラミング や 計算機による定理証明技術 |
| 学習の到達目標 | 文章による数学的な主張を論理式で表せる．証明法をふまえて証明を構成できる．意味論に基づいて命題の真偽を判定できる．形式体系の推論規則を使って証明できる．自動証明の基本である導出原理を具体例に適用して証明できる．数理論理学の応用について説明できる． |
| ディプロマ・ポリシー |
|
| 授業の方法 | 講義 |
| 授業の特徴 | Moodle |
| 教科書 | 授業のホームページで指定する． |
| 参考書 | 『数学は言葉』，新井紀子，東京図書，2009． 『記号論理入門 [新装版]』，前原昭二，日本評論社，2005． 『情報科学における論理』，小野寛晰，日本評論社，1994． |
| 成績評価方法と基準 | 期末試験10割．講義への10回以上の出席が期末試験の受験資格．チャレンジ問題による加点あり．6割以上の得点で合格． |
| オフィスアワー | 水曜日7〜8時限 (14:40-16:10)，情報棟5階 山田講師室 |
| 受講要件 | 集合論（集合，関係，順序，写像）や帰納的定義について理解していること．必要に応じて，「離散数学」の教科書で復習すること． |
| 予め履修が望ましい科目 | 離散数学，論理設計及び演習 |
| 発展科目 | データ構造・アルゴリズム論，オートマトン・形式言語理論，計算理論，計算機言語論 I |
| 授業改善への工夫 | 毎回の確認問題で受講生の理解度を把握し，授業の進度を調整する．確認問題の答案に授業への意見も書いてもらい，授業の進め方を改善する．ウェブを活用して授業の情報や資料を見られるようにする．Moodle を出席状況と採点結果の通知に使う． |
| その他 |
授業のホームページ（メールによる連絡先等も掲載） http://www.cs.info.mie-u.ac.jp/~toshi/lectures/mathlogic/ |
| キーワード | 命題論理，述語論理，形式体系，自然演繹，導出原理 |
|---|---|
| Key Word(s) | propositional logic, predicate logic, formal systems, natural deduction, resolution principle |
| 学習内容 | ●第１回 数理論理学の基礎 数理論理学の目的，形式化，数理論理学の応用 ●第２回 論理式と証明法 1 命題と述語，論理記号，論理式，真理値表 ●第３回 論理式と証明法 2 論理式の真偽，含意の直接証明，含意の意味 ●第４回 論理式と証明法 3 含意の間接証明，同値の証明，量化記号，全称と存在の基本表現 ●第５回 論理式と証明法 4 述語と集合の対応，全称と存在の慣用表現 ●第６回 論理式と証明法 5 集合と論理，全称と存在の証明，論理法則の利用と反証，全称と存在の否定 ●第７回 論理式と証明法 6 同値変形，全称と存在の併用 ●第８回 自然演繹 1 自然演繹の基礎，帰納的定義 ●第９回 自然演繹 2 述語論理の構文論，証明の形式化 ●第10回 自然演繹 3 命題論理の形式体系 ●第11回 自然演繹 4 述語論理の形式体系 ●第12回 述語論理の意味論 1 自然演繹の健全性と完全性，構造による言語の意味付け ●第13回 述語論理の意味論 2 恒真性と充足可能性 ●第14回 導出原理 1 導出原理（命題論理） ●第15回 導出原理 2 導出原理（述語論理） ●第15回の空き時間 数理論理学の応用 論理型プログラム言語，証明支援システム，定理自動証明器，ソフトウェアの正当性検証 |
| 事前・事後学修の内容 | 授業前に学習事項を確認し，教科書や配布資料を読んで疑問点を整理しておく．ウェブページ上の確認問題や演習問題を解き，理解度を確認する．復習には，授業中に解けなかった確認問題や配布資料の演習問題を解き，ウェブページの解答や解説を参考にするとよい． |
| ナンバリングコード(試行) |
|---|
※最初の2文字は開講主体、続く4文字は分野、最後の数字は開講レベルを表します。 ナンバリングコード一覧表はこちら