課程內(nèi)容：

本課程解釋了如何利用邏輯的實(shí)現(xiàn)來解決許多問題，如快速解決最難的數(shù)獨(dú)謎題、分析雙人游戲或查找計(jì)算機(jī)系統(tǒng)中的嚴(yán)重錯(cuò)誤。

課程目標(biāo)：

本課程旨在讓學(xué)生了解（數(shù)理）邏輯的基本原理以及邏輯在現(xiàn)代計(jì)算機(jī)科學(xué)中的一些應(yīng)用，包括硬件驗(yàn)證、有限域約束滿足和并發(fā)系統(tǒng)驗(yàn)證。

教學(xué)大綱：

- 命題邏輯

- 連接正則表達(dá)式（CNF）

- DPLL 可滿足性算法

- 隨機(jī)可滿足性算法

- 使用 BDT/BDDs/OBDDs 的布爾函數(shù)緊湊表示法

- 量化布爾邏輯 (QBF) 的拆分和 DPLL 算法

- 有限域命題邏輯

- 狀態(tài)變化系統(tǒng)

- 線性時(shí)態(tài)邏輯 (LTL)

- 模型檢查

學(xué)習(xí)成果：

成功完成本課程后，學(xué)生將能夠：

1、掌握命題邏輯的基本推理（或可滿足性檢查）算法。

2、掌握量化布爾公式的知識(shí)，基本了解約束變量和量詞。

3、了解 BDDS（二元判定圖）是一種緊湊表示命題公式的數(shù)據(jù)結(jié)構(gòu)。

4、了解命題邏輯的應(yīng)用（如有限域約束滿足和規(guī)劃），并能應(yīng)用命題邏輯解決困難的組合問題。

5、掌握簡(jiǎn)單時(shí)態(tài)邏輯的知識(shí)。

6、將有限狀態(tài)并發(fā)系統(tǒng)正式指定為過渡系統(tǒng)。

7、用時(shí)態(tài)邏輯指定簡(jiǎn)單轉(zhuǎn)換系統(tǒng)的屬性。