2015 年度 数理論理学 講義資料 (0) 青戸 等人 (新潟大学 自然科学研究科) 目次 - 講義の情報 - 講義の概要 1/7 情報論理学 講義情報 (1) 講義の進め方 スラ イ ド 教材あり ． 講義ホームページよ り ダウ ン ロ ード 可能． 演習問題あり ． 講義と 間を おかずに復習する こ と ． 講義の最初に 前回の問題の解答を 説明する ． 教科書・ 参考書 教科書： なし 参考書： 前原昭二著「 記号論理入門」 (日本評論社) 小野寛晰著「 情報科学における 論理」 (日本評論社) 2/7 そ の他の (英語の) 参考書 定評のある 参考書は前出の小野先生の本の最後を 参照． • 講義の内容に近い参考書： 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. 3/7 情報論理学 講義情報 (2) 講義ホームページ (暫定版) https://bitbucket.org/tkhtaoto/15logic/ オ フ ィ スア ワ ー 後日連絡 成績評価の方法 • 主に期末試験の結果によ っ て 評価する ． • 期末試験での持ち 込み ノ ート ・ 印刷物・ 参考書は持ち 込み可． iPad,PC 等の (通信可能な ) 機器は持ち 込み不可． 4/7 目次 - 講義の情報 - 講義の概要 情報論理学 講義概要 講義の目的 数理論理学は， 情報科学分野全般における 数学的・ 理 論的な思考技術の基本と し て ， 更にま た， ソ フ ト ウェ ア 科学 におけ る 形式的技法の基礎と し て 重要である ． こ のよ う な 観点から ， 数理論理学の基礎を 修得する こ と を 目的と する ． 講義の概要 数理論理学の基本である 命題論理およ び述語論理につ いて ， 命題の形式化， 命題の解釈法， ト ート ロ ジ ー， 論理 的同値性， 形式的推論法， 形式的証明と 数学的論証の対応， 意味論， 健全性と 完全性など について 講義する ． 4/7 情報論理学 講義計画 • • • • • • • • • • 命題論理の意味論 命題論理式の同値変形 帰納的定義 命題論理における 自然演繹法 命題論理における 健全性と 完全性 述語論理式の同値変形 述語論理における 自然演繹法 形式的証明と 数学的論証の対応 第一階述語論理の意味論 述語論理における 健全性と 完全性 最も 応用範囲が広く ， 最も 基本的な数理論理学の基礎を 身につける ． 5/7 (補足) 論理学は先端的な研究で応用さ れて いないの？ いく つかの主要な応用を 挙げる ： (1) 対話的証明器 数学の証明を 形式的に記述する ソ フ ト ウ ェ ア． 今ま で人 間の手で書かれて いた証明では大幅に省略さ れる が， こ れ を 計算機上で厳密に (プロ グ ラ ム のよ う に ) 記述． バグ のな い証明が可能になる ばかり でなく ， 推論シ ス テム の出力検 証やユーザー本位の定理証明への応用など ． (2) SAT/SMT ソ ルバー 計算困難な論理式の充足可能性を 高速に解く ソ フ ト ウ ェ ア． 高速に 解け る と は限ら ないが， 実は， 人間が解き たい 問題はかなり 高速に解ける こ と が多い． さ ま ざま な問題を6/7， 論理式等でエン コ ード し て ， SAT/SMT ソ ルバーを 用いる こ と で， 解を 高速に発見する こ と ができ る ． (3) モデルチェッ カ ー ソ フ ト ウ ェ ア のバグを 見つける のにさ ま ざま な入力を 試 す のではなく ， ど のよ う に動作し て 欲し いか (仕様) を 論理 を 用いて 記述し ， プロ グ ラ ム の入力や実行を 抽象化す る こ と でモ デルを 構築し ， モ デルが仕様を 満たす かを 検査す る こ と で， あら ゆる 入力や動作で (そ の仕様について ) 問題が ないかど う かを 判定する ． 情報 ＋ 論理 を 背景と し たア プ ロ ーチ は， Logic in Computer Science と よ ばれて おり ， 情報科学／情報工学 の基本的な分野の重要な柱の 1 つ． 7/7
© Copyright 2024 ExpyDoc
