2020 年度 数理論理学 講義資料 (0)
青戸 等人 (知能情報システムプログラ ム)
目次
- 講義の情報 - 講義の概要
1/9
数理論理学 講義情報 (1) 講義の進め方
スラ イ ド 教材あり ．
学務情報システムから の連絡に添付．
講義ホームページから も ダウ ン ロード 可能．
講義時間に講義ビデオを Youtubeで視聴し て く ださ い．
学務情報システムで URLを 前日〜当日に連絡．
講義のと き に用意する も の．
スラ イ ド 教材， ノ ート ， 筆記具
講義の途中に演習問題を 解く 必要あり ． 演習問題およ び解答あり ．
講義と 間を おかずに復習する こ と ．
いく つかの演習問題を レ ポート に課す．
教科書・ 参考書
教科書： なし 参考書：
前原昭二著「 記号論理入門」 (日本評論社)
小野寛晰著「 情報科学における 論理」 (日本評論社)
3/9
そ の他の ( 英語の ) 参考書
定評のある 参考書は前出の小野先生の本の最後を 参照．
• 講義の内容に近い参考書： Dirk van Dalen, Logic and Structure (3rd ed.), Springer-Verlag, 1991.
• ト ピッ ク も 広く 書き 方も 非常に 優れた参考書 (ただ し ， 数学書の読み方に慣れて いないと 難し い)： Herbert B.
Enderton, A Mathematical Introduction to Logic (3rd ed.), Academic Press, 2001.
• プログラ ムを 使っ て説明し ている 本(プログラ ム好き の 人には良いかも )： John Harrison, Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, 2009.
数理論理学 講義情報 (2) 講義ホームページ
http://www.nue.ie.niigata-u.ac.jp
/˜aoto/lecture/Logic/
(講義資料や連絡など ． 随時更新予定)
オフ ィ スア ワ ー
Slack上で行いま す． 登録先を お知ら せし ま すので， 希 望者は参加し て く ださ い．
成績評価の方法
•期末試験(50%)， レ ポート 課題(50%)で評価．
•期末試験はオン ラ イ ン で実施の予定
ノ ート ・ 印刷物・ 参考書・ PC等持ち 込み可．
他人と の相談は不可． 同じ 部屋での受験も 不可． 5/9
講義の復習と レ ポート
• 復習： 毎回の講義はそ れ以前の講義内容の理解を 前提と し ま す． 講義について 行く には， 毎回， 講義内容を 余さ ず消化する こ と が重要です． 不明な点は復習し ， 演習問 題を 解いて 理解を 確実にし て おく こ と ．
• 講義のホームページに， スラ イ ド ， 演習問題， 演習問題 の解答を 掲載し ま す． 解答のチェッ ク は， 自分でやっ てく ださ い． 講師の方では採点し ま せん．
• レ ポート : いく つか問題を 選んで， レ ポート 問題にし ま す． 学務情報システムでレ ポート 課題を 出し ま すので， 期 限ま でに， 学務情報シ ステムから ， 丸付け済みの解答の 写真を ア ッ プロード し て く ださ い．
目次
- 講義の情報 - 講義の概要
数理論理学 講義概要 講義のねら い
数理論理学は， 情報分野全般における 数学的・ 理論的 な思考技術の基本と し て ， 更にま た， ソ フ ト ウ ェ ア 科学/計 算論/人工知能分野等における 基礎と し て重要である ． こ の よ う な観点から ， 数理論理学の基礎を 修得する こ と を 目的 と する ．
講義の概要
数理論理学の基本である 命題論理およ び述語論理につ いて ， 構文論と 意味論を 紹介する ． 具体的には，．．． など に ついて 講義する ．
数理論理学 講義計画
• 命題論理の意味論
• 命題論理式の同値変形
• 帰納的定義
• 命題論理における 自然演繹法
• 命題論理における 健全性と 完全性
• 述語論理式の同値変形
• 述語論理における 自然演繹法
• 形式的証明と 数学的論証の対応
• 第一階述語論理の意味論
• 述語論理における 健全性と 完全性
最も 応用範囲が広く ， 最も 基本的な数理論理学の基礎を 身につける ．
7/9
(補足) 論理学は先端的な研究で応用さ れて いないの？
いく つかの主要な応用を 挙げる ： (1) 対話的証明器
数学の証明を 形式的に記述する ソ フ ト ウ ェ ア． 今ま で人 間の手で書かれて いた証明では大幅に省略さ れる が， こ れ を 計算機上で厳密に (プロ グラ ムのよ う に)記述． バグのな い証明が可能になる ばかり でなく ， 推論シ ステムの出力検 証やユーザー本位の定理証明への応用など ．
(2) SAT/SMTソ ルバー
計算困難な論理式の充足可能性を 高速に解く ソ フ ト ウ ェ ア． 高速に解ける と は限ら ないが， 実は， 人間が解き たい 問題はかなり 高速に解ける こ と が多い． さ ま ざま な問題を ，
論理式等でエン コ ード し て ， SAT/SMTソ ルバーを 用いる こ と で， 解を 高速に発見する こ と ができ る ．
(3) モデルチェッ カー
ソ フ ト ウ ェ ア のバグを 見つける のにさ ま ざま な入力を 試 すのではなく ， ど のよ う に動作し て 欲し いか(仕様)を 論理 を 用いて 記述し ， プロ グラ ムの入力や実行を 抽象化する こ と でモデルを 構築し ， モデルが仕様を 満たすかを 検査する こ と で， あら ゆる 入力や動作で (そ の仕様について)問題が ないかど う かを 判定する ．
情報 ＋ 論理 を 背景と し たア プロ ーチは， Logic in Computer Science と よ ばれて おり ， 情報科学／情報工 学の基本的な分野の重要な柱の1つ．
9/9
