| 課程編碼 Course Code | 中文課程名稱 Course Name (Chinese) | 英文課程名稱 Course Name (English) | 總學分數 Credits | 總時數 Hours |
|---|---|---|---|---|
| C725004 | 計算邏輯與軟體驗證 | Computational Logic and Software Verification | 3.0 | 3 |
| 中文概述 Chinese Description | 數理邏輯是理論計算機科學各領域重要的基礎。在本課程中，重點關注於數理邏輯在軟體程式驗證與機器可檢驗之證明等的應用。透過各種如SAT/SMT求解器與輔助證明工具Coq等，本課程將涵蓋以下主題：比例邏輯、一階邏輯、可滿足性模組理論、模型檢查與程式驗證。 | |||
| 英文概述 English Description | Mathematical logic is an important foundation of various fields in theoretical computer science. This course focuses on its applications from software/program verification to machine-checkable proofs. Through various tools like SAT/SMT solvers and proof-assistant Coq, this course will cover the following topics: proportional logic, first-order logic, satisfiability module theory, model checking and program verification. | |||
備註：