[Back to Teaching]
応用論理 Applied Logic (2016年度)
概要 Basics
- S1ターム 月曜3限 13:00 - 14:45.
Mondays 13:00 - 14:45, S1 Term.
- 理学部7号館 007号室.
Room 007, School of Science Bldg. No. 7 (map)
- 理学部情報科学科 4年生 選択必修 時間割コード： 0510084
担当教員 Lecturer
- 蓮尾 一郎 准教授 （理学部情報科学科）．
Ichiro Hasuo, Associate Professor, Dept. Information Science, Faculty of Science.
講義の目的 Course Objectives
- プログラムや計算機システムの仕様記述・形式検証の理論について講義を行う．特に，時相論理式による仕様記述と，ωオートマトンを用いたモデル検査アルゴリズムについて解説する．
Understand the theory of formal specification and verification of computer programs and systems. Specifically you will learn about: formal specification by temporal logic formulas; and model checking via omega-automata.
講義の方法 Teaching Methods
教科書と，各回に配布するハンドアウトに基づき，板書で行う．
- 配布する教科書およびハンドアウトに基づいて，板書で説明する．配布資料および板書は英語，口頭説明は日本語または英語．
Textbooks and handouts will be distributed; they are in English. Boards are in English too; oral explanations are either in Japanese or in English.
- 各回の内容は，前回の講義時に配布するハンドアウトの中で予告する．予習が推奨される．(ぜひ，少なくとも，電車の中でざっと眺めてきてください)
Topics for the next lecture will be announced in handouts, in advance. It is highly recommended that you do some preparatory reading before lectures. (A quick glance is better than none.)
- 時々出題するレポート課題(下参照)は，復習問題が1つ，予習問題が1つ．
Report assignments will be given occasionally; they consist of review questions (for what has been already covered in lectures) and preparatory questions (for what is to come). See below for further details.
教科書・ハンドアウト Reading Materials
このページで配布する資料は，すべて学内のみからアクセス可能．
The links here work only from within the UTokyo domain.
- 教科書: 次の2つを用いる．Textbooks:
- Moshe Y. Vardi: An Automata-Theoretic Approach to Linear Temporal Logic. Banff Higher Order Workshop 1995: 238-266
- S. Demri and P. Gastin. Specification and Verification using Temporal Logics. In Modern applications of automata theory, IISc Research Monographs 2, chapter 15, pages 457-494. World Scientific, 2012.
- 毎回のハンドアウト: 下の「スケジュール」の項を参照．
Links to handouts are found below, in the "Schedule" section.
評価 Evaluation
以下の要素により，総合的に判断する．
The following points will be taken into account.
- 毎回のレポート課題
Report assignments in lectures
- 出席確認を兼ねる．
- 毎週，講義開始前に直接提出．講義開始後は一切受け取らない．
Your reports must be handed in before a lecture starts.
- A4用紙に手書きか，出力したものを提出．
On A4 papers. They can be hand-written, or printed.
- 想定ワークロード: 講義時間の他に，予習・復習・レポートで1.5時間から3時間．
Expected workload: 1.5--3 hours each week, besides lectures.
- 期末レポート （最終回ハンドアウトで指定）．
Course-end report assignment (specified at the last lecture)
不正行為には厳正に対処します．(たとえば法学部ならば一発退学)
「不正行為」の定義について，小林直樹先生のページから抜粋:
レポートは，自分で考えたこと，調べたことを，自分の言葉でまとめること．レポートをまとめるにあたって，参考にした文献があれば，レポート中の各個所について参考文献へのレファレンスを挿入するとともに，レポートの最後に参考文献リストをつけること．また，文献の一部をそのまま引用する場合には，引用部分を明確にするために引用符とレファレンスをつけること（レポートの最後に参考文献として載せるだけでは不十分）．参考文献から図や写真，プログラム等を引用する場合も同様．
以上が守られない場合には，提出されたレポートは盗作と判断され，深刻な結果に至る可能性があります．
なお，何をもって盗作と判断されるかを知る上で，例えばインディアナ大学のこちらのページ に目を通すことをお勧めします．理解を確認するためのクイズを解くことができます．
Note that plagiarism is taken extremely seriously. You should know what exactly would comprise plagiarism; here is a useful information source.
スケジュール Schedule