[前へ戻る]
   

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

関連するディプロマポリシー Related Diploma Policy
時代の課題と社会の要請に応えた専門的知識と技能/Expert knowledge and skills to address the issues of the age and the demands of society
 
到達目標 Target to be Reached
計算機科学において論理学は様々な目的で用いられるが、近年はプログラムの正当性を検証するために有効な様々な論理が提案されている。この科目では、論理学を用いてプログラムの正当性を証明できるようになることを目標とする。論理の例としては、古典命題論理や古典一階述語論理など基本となる論理の確認から始め、様相論理、不動点論理、ホーア論理など発展的な論理を使えるようになることを目指す。

また、論理と代数の間には対応があるため、ブール代数や様相代数など代数として論理を理解することも目標とする。代数と論理を理解することによって、高等学校までの「数学」における命題や証明について厳密に表現できるようになるだけでなく、種々の定義についても、盲目的に覚えるのではなく「なぜそのように定義する必要があったのか」も含めて深く理解し他人に説明できるようになる。したがって、この科目は高等学校の数学教育にも還元できる科目である。

 
授業内容 Course Content
前半は古典命題論理や古典一階述語論理など基本となる論理の意味論と、形式体系の一つである自然演繹を学ぶ。後半では、様相論理、不動点論理、プログラムの正当性証明のためのホーア論理など発展的な論理を学ぶ。
 
授業計画 Course Planning
第2回以降についての資料は事前に配布する。予習として、毎週指定される問題について解いてくることが不可欠である。復習として、講義中の他の学生の発表内容や教員からの指摘内容を確認し、ノートを清書してくることも不可欠である。予習・復習併せて各回あたり4時間の自己学習を想定している。

第1回: シラバスの記載事項の確認、命題論理の意味論、集合
第2回: 命題論理の自然演繹
第3回: 一階述語論理の意味論、整数の性質、等式の証明
第4回: 一階述語論理の自然演繹
第5回: 全称の除去
第6回: 存在の導入
第7回: 存在の除去
第8回: 全称の導入
第9回: 様相論理の意味論
第10回: 様相論理の形式体系と様相代数
第11回: 不動点論理の意味論
第12回: 不動点論理の形式体系
第13回: プログラムの正当性の形式的証明
第14回: 総復習、計算と論理と代数の概観

 
授業運営 Course Management
受講者は、毎週指定される問題について解いたうえで講義に臨み、授業中に白板を使って説明する、という流れとなる。教員の質問に答えられない場合は、答えられるようになるまで何度でも復習が必要となる。
 
評価方法 Evaluation Method
毎回の発表内容で100%評価する。
 
オフィスアワー Office Hour (s)
西澤准教授:木曜日12:40~14:00(6-418室)
   あるいはnishizawa@kanagawa-u.ac.jpまで(常時)。


 
使用書 Textbook (s)
適宜資料を配布する。
参考書 Book (s) for Reference
James L.Hein (著), 神林 靖 (翻訳)『独習コンピュータ科学基礎II 論理構造』[翔泳社]2011

 
 
 
[前へ戻る]