宗旨

近年來，從事基礎計算科學研究之台灣學者們已在各校各自成立研究團隊並相互合作。對基礎計算科學有興趣之學生須透過一系列課程學習基本知識；然而，國內從事此類研究的學者分散在各校，難以僅靠一己之力開設整套課程。因此，我們邀請有相同興趣的學者一同開課，訓練下一代的研究人才。

「邏輯、語言與計算」暑期研習營希望培養學員獨立進行基礎計算科學研究之能力。從2008年起，本研習營在兩大主題之間輪流替換。今年之主題為邏輯與正規驗證。

自 2012 年起，本研習營正式成為台灣大學暑修課程，針對大學部學生開課，但亦歡迎研究生選修。台灣大學學生可透過國立台灣大學暑期課程網選課，有學籍之其他學校學生可透過校際選修選課。

「邏輯、語言與計算」暑期研習營從2007年開始至今每年舉辦，已舉辦八屆，今年為第九屆。

時間地點

日期：2015 年 7 月 6 日 (週一) 至 7 月 17 日 (週五)，共計十天。
時間：每週一至週五早上九點十分至下午五點二十分。
地點：
- 7/6(一)~7/16(四)：國立臺灣大學管理學院一號館101教室。
- 7/17(五)：國立臺灣大學管理學院一號館103教室。
- 從舟山路側門進入校園看到7-11右轉直走，經過華南銀行右前方建築即為管理學院一號館。

課程內容	講者	時數
型式邏輯簡介 Introduction to Formal Logic
命題邏輯 Propositional Logic	Anthony W. Lin 耶魯-新加坡國大學院	6
一階邏輯 First Order Logic	Anthony W. Lin 耶魯-新加坡國大學院	6
布林可滿足性及其應用 Boolean Satisfiability and Its Applications
布林可滿足性演算法 Boolean Satisfiability Algorithms	黃鐘揚 Chung-Yang (Ric) Huang 台灣大學電機工程學系	9
邏輯合成 Logic Synthesis	江介宏 Jie-Hong Roland Jiang 台灣大學電機工程學系	9
一階邏輯可滿足性及其應用 First Order Logic Satisfiability and Its Applications
Satisfiability Modulo Theories	陳郁方 Yu-Fang Chen 中央研究院資訊科學研究所	6
Quantified Linear Arithmetic	陳郁方 Yu-Fang Chen 中央研究院資訊科學研究所	6
Quantifier-Free Linear Arithmetic	王柏堯 Bow-Yaw Wang 中央研究院資訊科學研究所	6
Quantifier-Free Equality and Data Structures	蔡明憲 Ming-Hsien Tsai 中央研究院資訊科學研究所	6
Combining Decision Procedures	郁方 Fang Yu 政治大學資訊管理學系	6

以上課程(含演講54小時及考試3小時)共57小時，另預定進行專題討論約3小時。

注意: 本課程包含實習課，請自備筆記型電腦。

	7 / 6	7 / 7	7 / 8	7 / 9	7 / 10	7 / 13	7 / 14	7 / 15	7 / 16	7 / 17
9:00-12:00	Lin	Lin	黃	黃	江	陳	王	蔡	郁	考試
12:00-14:00	午休					午休
14:00-17:00	Lin	Lin	黃	江	江	陳	王	蔡	郁	專題討論

報名資格
1. 大學資訊、電機、數學相關學系在學學生，修業二年（含）以上，或
2. 大學資訊、電機、數學相關學系研究所在學學生，或
3. 專科或大學畢業，現從事資訊相關行業工作者。
招收人數：以 40 人為原則，未達 40 人得不開班。
報名日期：請見註冊繳費段落。
報名方式：請至請至國立台灣大學暑期課程網選課。

本課程於台灣大學暑期第一梯次開授，為三學分之選修課，正式課號與課名為：「725 U3510 自動化正規驗證」。

可至國立台灣大學暑期課程網辦理「外校學生上網報名」。

因場地限制，修課人數上限40人（含非台大學生），敬請把握時間，於時程內提早選課。