目錄表
教材下載
型式邏輯簡介 Introduction to Formal Logic
布林可滿足性及其應用 Boolean Satisfiability and Its Applications
一階邏輯可滿足性及其應用 First Order Logic Satisfiability and Its Applications
教材下載
型式邏輯簡介 Introduction to Formal Logic
命題邏輯 Propositional Logic
Introduction to Propositional Logic
Exercises:
Tutorial1
Constraint Programming
Exercises:
N-Queen and Sudoku example code
Normal Forms
一階邏輯 First Order Logic
First Order Logic
習題參考解答
Tutorial1 Solution
布林可滿足性及其應用 Boolean Satisfiability and Its Applications
布林可滿足性演算法 Boolean Satisfiability Algorithms
邏輯合成 Logic Synthesis
Homework:
Logic Synthesis Homework
[
Solution
]
一階邏輯可滿足性及其應用 First Order Logic Satisfiability and Its Applications
Before class
Install Z3 for Python
Z3 APIs
Satisfiability Modulo Theories and its Application in Software Verification
Exercise:
SMT
Quantifier Elimination for Presburger Arithmetic
Exercise:
Quantifier Elimination
[
Solution
]
References:
A DECISION PROCEDURE FOR THE FIRST ORDER THEORY OF REAL ADDITION WITH ORDER
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).
Quantifier-Free Linear Arithmetic
Exercises:
Simplex
[
Solution
]
Quantifier-Free Equality and Data Structure
Exercises:
Equality and Data Structure
Examples code using z3Py
Homework:
EUF, List, and Array
[
Solution
]
Decision Procedures An Algorithmic Point of View
(
pdf
,
CVC4 lab
,
lab code
,
reference text
)