※ 本文是否可提供台大同学转作其他非营利用途？（须保留原作者 ID）
（是／否／其他条件）：是
哪一学年度修课：109-1
ψ 授课教师 (若为多人合授请写开课教师，以方便收录)
王柏尧 教授
λ 开课系所与授课对象 (是否为必修或通识课 / 内容是否与某些背景相关)
资工系选修
δ 课程大概内容
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.
（以上复制自课程网）
整学期分为四个主题，分别介绍
1. propositional logic
2. predicate logic (first-order logic)
3. model checking (temporal logic)
4. program verification (Hoare logic)
每个主题都先从motivation开始（为什么CS的领域会需要它），
接着讲定义跟基本的操作，最后介绍相关的应用。
详情请见
https://homepage.iis.sinica.edu.tw/~bywang/courses/comp-logic/
Ω 私心推荐指数(以五分计) ★★★★☆
好课必须推
η 上课用书(影印讲义或是指定教科书)
教授自编投影片
μ 上课方式(投影片、团体讨论、老师教学风格)
投影片为主，板书为辅。
教授人很佛，讲解也很清楚，该区分清楚的地方也有区分清楚，
不像通识逻辑都把syntax跟semantics混在一起(#
σ 评分方式(给分甜吗？是扎实分？)
Homework 50% （共6次）
Midterm 20%
Final 20%
Attendence 10% （应该是送分）
给分很佛，最后46.43% A+，作业迟交也会收（但还是尽量准时啦
ρ 考题型式、作业方式
作业大致会是一次手写一次程式。
手写主要是练习一些基本的操作，
像是兜 natural deduction proof 或是把一些叙述转成逻辑的式子之类的。
程式的部分主要跟着介绍的 application，
propositional logic 是把 pigeon-hole problem encode 成 SAT，
predicate logic 是用 coq 证中国剩余定理，
temporal logic 是拿 NuSMV 来 model 一个 public-key protocol 的
man-in-the-middle attack，都很好玩。
考试跟手写差不多（简单一点？），而且可以 open book。
ω 其它(是否注重出席率？如果为外系选修，需先有什么基础较好吗？老师个性？
加签习惯？严禁迟到等…)
不点名，应该全签吧
教授是从中研院来传教(X)的，人很赞，有问题上/下课问都可以
理论上无基础可（可能要会写很简单的程式），
如果有修过离散、逻辑、自动机（计算理论）、算法之类的
在一些地方理解起来会比较快，不过没有也没关系
Ψ 总结
好课推推！