|
課程名稱 |
計算邏輯簡介
Introduction to Computational Logic |
|
開課學期 |
111-1 |
|
授課對象 |
電機資訊學院 資訊工程學系 |
|
授課教師 |
王柏堯 |
|
課號 |
CSIE4111 |
|
課程識別碼 |
902 48130 |
|
班次 |
|
|
學分 |
3.0 |
|
全/半年 |
半年 |
|
必/選修 |
選修 |
|
上課時間 |
星期三2,3,4(9:10~12:10) |
|
上課地點 |
資101 |
|
備註 |
限學士班二年級以上
總人數上限：40人 |
|
|
|
|
課程簡介影片 |
|
|
核心能力關聯 |
核心能力與課程規劃關聯圖 |
|
課程大綱
|
|
為確保您我的權利,請尊重智慧財產權及不得非法影印
|
|
課程概述 |
This course gives a general introduction to mathematical logic and its applications in computer science. Mathematical logic is an important foundation of various fields in theoretical computer science. It also has many important applications from program verification to machine-checkable proofs. Through various tools, this course gives a gentle introduction of logic in computer science. It also covers preliminaries for theoretical topics in advanced courses. |
|
課程目標 |
To introduce students skills of logical reasoning.
To introduce students elements of mathematical logic.
To introduce students applications of mathematical logic in computer science. |
|
課程要求 |
待補 |
|
預期每週課後學習時數 |
|
|
Office Hours |
|
|
指定閱讀 |
|
|
參考書目 |
1. Logic in Computer Science: Modelling and Reasoning about Systems, M. Huth and M. Ryan, Cambridge University Press, 2004.
2. Handbook of Theoretical Computer Science (volume B). The MIT Press, 1994.
3. The SAT Live! homepage. http://www.satlive.org
4. The SMT-LIB homepage. http://www.smtlib.org
5. The Coq Proof Assistant homepage. http://coq.inria.fr
6. The NUSMV homepage. http://nusmv.fbk.eu/ |
|
評量方式
(僅供參考) |
|
|
週次 |
日期 |
單元主題 |
|
Week 00 |
09/07 |
no class |
|
Week 01 |
09/14 |
propositional logic, natural deduction (propositional logic) |
|
Week 02 |
09/21 |
normal form, SAT solvers |
|
Week 03 |
09/28 |
no class |
|
Week 04 |
10/05 |
predicate logic, natural deduction (predicate logic) |
|
Week 05 |
10/12 |
semantics, undecidability, expressiveness |
|
Week 06 |
10/19 |
Coq |
|
Week 07 |
10/26 |
MIDTERM |
|
Week 08 |
11/02 |
linear temporal logic |
|
Week 09 |
11/09 |
NuSMV |
|
Week 10 |
11/16 |
branching-time logic |
|
Week 11 |
11/23 |
model checking algorithms (CTL, LTL) |
|
Week 12 |
11/30 |
model checking algorithms (LTL) |
|
Week 13 |
12/07 |
program verification, proof rules (Hoare logic) |
|
Week 14 |
12/14 |
proof rules (Hoare logic) |
|
Week 15 |
12/21 |
FINAL |
|