[前へ戻る]
   

 授業科目
 Course Title
計算論理学特論
Computational Logic
 担当者
 Instructor
准教授 西澤 弘毅  後学期 金曜日1時限
 単 位
 Credit
2

到達目標 Target to be Reached
本講義の到達目標は、受講生が厳密な数学的証明を書けるようになることである。
特に、「任意」と「存在」の量化子を扱える一階述語論理に基づいた証明と、
情報分野でよく現れる「構造に関する帰納法」について、正しい証明を
書けるようになることが目標である。最後に情報分野の応用例として、
プログラムの正当性の厳密な証明の仕方も学ぶ。
なお、この科目は、経営工学専攻のカリキュラムポリシーに基づき、本領域の
4部門のうち数理情報システム工学の部門の科目としての教育目標を達成するために
開講される。
 
授業内容 Course Content
この講義では、下記の使用書に沿って、形式的な証明とは何か、
という根本的な疑問から始め、基本的な論理による証明の仕方を学ぶ。
記号論理学の本来の目的は論理を分析することだが、本講義では論理はあくまでも道具として
使い、情報分野で求められる数学的証明を厳密に書く方法を学ぶ。
 
授業計画 Course Planning
以下の内容を順に学ぶ。ただし、進捗状況により内容は前後する。
2回目以降は、予習として配付資料の各回の該当ページをあらかじめ読んでくることを前提とする。

1. 命題論理の意味論
2. 命題論理の自然演繹
3. 証明
4. 導出される証明
5. 命題論理の自然演繹の演習
6. 一階述語論理の意味論
7. 一階述語論理の自然演繹
8. 全称の除去
9. 存在の導入
10. 存在の除去
11. 全称の導入
12. 等価性の論理
13. 構造に関する帰納法
14. プログラムの正当性の形式的証明
15. 総復習の演習

 
授業運営 Course Management
受講者は、毎週指定される問題について解いたうえで講義に臨み、授業中に白板を使って説明する、
という流れとなる。教員の質問に答えられない場合は、答えられるようになるまで何度でも
復習が必要となる。

 
評価方法 Evaluation Method
総復習の試験100%で評価する。ただし、毎週の演習状況が良い場合、それを加味して
評価を上げる場合がある。
 
オフィスアワー Office Hour (s)
水曜日 12:10~13:30(6-418室)
 
使用書 Textbook (s)
適宜資料を配布する。
参考書 Book (s) for Reference
独習コンピュータ科学基礎II 論理構造『James L.Hein (著), 神林 靖 (翻訳)』[翔泳社]2011年

 
 
 
[前へ戻る]