目錄表
教材下載
型式邏輯簡介 Introduction to Formal Logic
- 命題邏輯 Propositional Logic
-
- Exercises: Tutorial1
-
- Exercises: N-Queen and Sudoku example code
-
- 一階邏輯 First Order Logic
- 習題參考解答
布林可滿足性及其應用 Boolean Satisfiability and Its Applications
-
- Homework: Logic Synthesis Homework [Solution]
一階邏輯可滿足性及其應用 First Order Logic Satisfiability and Its Applications
- Before class
-
- Exercise: SMT
-
- Exercise: Quantifier Elimination[Solution]
-
- The paper introduces quantifier elimination procedure for FOL with theory of Presburger arithmetics over rational and real numbers (the same procedure works over both domains).
-
-
- Exercises: Equality and Data Structure
- Homework: EUF, List, and Array[Solution]