数理論理学 講義情報 (1) 講義の進め方

2020 年度 数理論理学 講義資料 (0)

青戸 等人(知能情報システムプログラ ム)

目次

1/9

数理論理学 講義情報 (1) 講義の進め方

スラ イ ド 教材あり ．

学務情報システムから の連絡に添付．

講義ホームページから も ダウ ン ロード 可能．

講義時間に講義ビデオをYoutubeで視聴し て く ださ い．

学務情報システムでURLを 前日〜当日に連絡．

講義のと き に用意する も の．

スラ イ ド 教材， ノ ート ， 筆記具 講義の途中に演習問題を 解く 必要あり ． 演習問題およ び解答あり ．

講義と 間を おかずに復習する こ と ． いく つかの演習問題を レ ポート に課す．

2/9

教科書・ 参考書

前原昭二著「 記号論理入門」(日本評論社) 小野寛晰著「 情報科学における 論理」(日本評論社)

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.

4/9

数理論理学 講義情報 (2) 講義ホームページ

http://www.nue.ie.niigata-u.ac.jp

/˜aoto/lecture/Logic/

(講義資料や連絡など ． 随時更新予定)

オフ ィ スア ワ ー

Slack上で行いま す． 登録先を お知ら せし ま すので， 希 望者は参加し て く ださ い．

成績評価の方法

•期末試験(50%)， レ ポート 課題(50%)で評価．

•期末試験はオン ラ イ ン で実施の予定

ノ ート ・ 印刷物・ 参考書・ PC等持ち 込み可．

他人と の相談は不可． 同じ 部屋での受験も 不可． _5/9

講義の復習と レ ポート

•復習： 毎回の講義はそ れ以前の講義内容の理解を 前提と し ま す． 講義について 行く には， 毎回， 講義内容を 余さ ず消化する こ と が重要です． 不明な点は復習し ， 演習問 題を 解いて 理解を 確実にし て おく こ と ．

•講義のホームページに， スラ イ ド ， 演習問題， 演習問題 の解答を 掲載し ま す．解答のチェッ ク は， 自分でやっ てく ださ い． 講師の方では採点し ま せん．

•レ ポート: いく つか問題を 選んで， レ ポート 問題にし ま す．学務情報システムでレ ポート 課題を 出し ま すので， 期 限ま でに， 学務情報シ ステムから ， 丸付け済みの解答の 写真を ア ッ プロード し て く ださ い．

6/9

目次

数理論理学 講義概要 講義のねら い

 数理論理学は， 情報分野全般における 数学的・ 理論的 な思考技術の基本と し て ， 更にま た，ソ フ ト ウ ェ ア 科学/計 算論/人工知能分野等における 基礎と し て重要である ． こ の よ う な観点から ， 数理論理学の基礎を 修得する こ とを 目的 と する ．

講義の概要

 数理論理学の基本である命題論理およ び述語論理につ いて ， 構文論と 意味論を 紹介する ． 具体的には，．．． など に ついて 講義する ．

6/9

数理論理学 講義計画

•命題論理の意味論

•命題論理式の同値変形

•帰納的定義

•命題論理における 自然演繹法

•命題論理における 健全性と 完全性

•述語論理式の同値変形

•述語論理における 自然演繹法

•形式的証明と 数学的論証の対応

•第一階述語論理の意味論

•述語論理における 健全性と 完全性

最も 応用範囲が広く ， 最も 基本的な数理論理学の基礎を 身につける ．

7/9

(補足) 論理学は先端的な研究で応用さ れて いないの？

いく つかの主要な応用を 挙げる ： (1)対話的証明器

数学の証明を 形式的に記述する ソ フ ト ウ ェ ア． 今ま で人 間の手で書かれて いた証明では大幅に省略さ れる が， こ れ を 計算機上で厳密に(プロ グラ ムのよ う に)記述． バグのな い証明が可能になる ばかり でなく ， 推論シ ステムの出力検 証やユーザー本位の定理証明への応用など ．

(2)SAT/SMTソ ルバー

計算困難な論理式の充足可能性を 高速に解く ソ フ ト ウ ェ ア． 高速に解ける と は限ら ないが， 実は， 人間が解き たい 問題はかなり 高速に解ける こ と が多い． さ ま ざま な問題を ，_8/9

論理式等でエン コ ード し て ， SAT/SMTソ ルバーを 用いる こ と で， 解を 高速に発見する こ と ができ る ．

(3)モデルチェッ カー

ソ フ ト ウ ェ ア のバグを 見つける のにさ ま ざま な入力を 試 すのではなく ， ど のよ う に動作し て 欲し いか(仕様)を 論理 を 用いて 記述し ， プロ グラ ムの入力や実行を 抽象化する こ と でモデルを 構築し ， モデルが仕様を 満たすかを 検査する こ と で， あら ゆる 入力や動作で(そ の仕様について)問題が ないかど う かを 判定する ．

情報 ＋ 論理 を 背景と し たア プロ ーチは， Logic in Computer Science と よ ばれて おり ， 情報科学／情報工 学の基本的な分野の重要な柱の1つ．

9/9