論理学 2c

更新日:2017-03-11

時間割コード

1000093

ナンバリングコード

SIS-03-2005-J

区分

専門基礎科目

単位数

CS必修1単位

開講形態

講義

対象学年

2年

学期 曜日 時間 集中講義の有無

秋2期 金曜2限目

講義室

IB館講義室

開講系

CS

担当教員 所属

結縁 祥治、中澤 巧爾

所属

CS・情報システム

メールアドレス

yuen@i.nagoya-u.ac.jp (結縁)
knak@i.nagoya-u.ac.jp (中澤)

オフィスアワー

事前にメールでアポイントメントをとること

授業概要

論理学1において学んだ基礎論理学にもとづいて,コンピュータ科学における論理学の適用技法について習得する。(1)SATソルバなどの制約解消系による充足可能性判定による問題解決,(2)導出原理による証明に基づく論理型プログラミングの基礎,および(3)ホーア論理に代表されるプログラム論理によるプログラムの検証について講義を行う。

◆講義目的

コンピュータ科学において理論・応用両面で重要な役割を果たす論理学の基礎とその適用技法について学ぶ。とくに,ソフトウェア科学において論理学のアイディアがどのように利用されているかを理解する。

◆授業内容

論理学1において学んだ基礎論理学にもとづいて,コンピュータ科学における論理学の適用技法について解説する。とくに,(1)SATソルバなどを用いた充足可能性判定による問題解決,(2)導出原理による証明に基づく論理型プログラミングの基礎,および(3)ホーア論理に代表されるプログラム論理によるプログラム検証について学ぶ。

1. ガイダンスと数学的準備 
2. 命題論理式の充足可能性判定 
3. SATソルバによる問題解決 
4. エルブランの定理 
5. 導出原理と論理型プログラミング 
6. プログラミング言語のモデルと意味論 
7. ホーア論理 
8. 総括

◆教科書・参考文献・履修条件等

必要に応じて資料を配布する。

◆授業期間中の課題・宿題等

講義において説明した理論を理解するために課題を与える。

成績評価方法・基準

講義中に与える演習課題の評価60%,期末試験40%.合計100点満点で60点以上を合格とする。

Course Title

Logic 2c

Class Timetable Code

1000093

Numbering Code

SIS-03-2005-J

Course Category

Basic Specialized Courses

Credits

Compulsory [Department of Computer Science]1

Class Format


Grade

2

Semester, Day and Period

Autumn 2 semester Friday2

Instructor(s)


Affiliation


Mailaddress

yuen@i.nagoya-u.ac.jp (結縁)
knak@i.nagoya-u.ac.jp (中澤)

Course Topics


Course Purpose


Course Contents


Textbooks, Reference Materials and Requirements


Assignment


Grading Criteria