近年來,從事基礎計算科學研究之台灣學者們已在各校各自成立研究團隊並相互合作。對基礎計算科學有興趣之學生須透過一系列課程學習基本知識;然而,國內從事此類研究的學者分散在各校,難以僅靠一己之力開設整套課程。因此,我們邀請有相同興趣的學者一同開課,訓練下一代的研究人才。
「邏輯、語言與計算」暑期研習營希望培養學員獨立進行基礎計算科學研究之能力。從2008年起,本研習營在兩大主題之間輪流替換。今年之主題為邏輯與正規驗證。
自 2012 年起,本研習營正式成為台灣大學暑修課程,針對大學部學生開課,但亦歡迎研究生選修。台灣大學學生可透過國立台灣大學暑期課程網選課,有學籍之其他學校學生可透過校際選修選課。
「邏輯、語言與計算」暑期研習營從2007年開始至今每年舉辦,已舉辦八屆,今年為第九屆。
課程內容 | 講者 | 時數 |
---|---|---|
型式邏輯簡介 Introduction to Formal Logic | ||
命題邏輯 Propositional Logic | Anthony W. Lin 耶魯-新加坡國大學院 | 6 |
一階邏輯 First Order Logic | 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 | ||
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 | 黃 | 江 | 江 | 陳 | 王 | 蔡 | 郁 | 專題討論 |
本課程於台灣大學暑期第一梯次開授,為三學分之選修課,正式課號與課名為:「725 U3510 自動化正規驗證」。
請至國立台灣大學暑期課程網選課。
可至國立台灣大學暑期課程網辦理「外校學生上網報名」。
因場地限制,修課人數上限40人(含非台大學生),敬請把握時間,於時程內提早選課。