Logics for Computer Science
| | topic | chapters | slides | assignment | results | solutions |
| 1 | Introduction. Propositional Logic. | | | | ||
| 2 | Propositional Logic. Satisfiability. | | | | ||
| 3 | Satisfiability Checking. | | | | ||
| 4 | Polarity. CNF | |||||
| 5 | CNF and clausal form. Unit propagation | | | | ||
| 6 | Optimised Definitional Transformation. DLL. | | | | ||
| 7 | SAT and Randomisation. | | | | ||
| 8 | Semantic Tableaux. | | | | ||
| 9 | BDDs and OBDDs | | | | ||
| 10 | OBDD Algorithms. | |||||
| 11 | Quantified Boolean Formulas. | | | | ||
| 12 | Quantified Boolean Formulas. | | | | ||
| 13 | Satisfiability Checking for QBF. | | | | ||
| 14 | Satisfiability Checking for QBF. | |||||
| 15 | Propositional Logic of Finite Domains. | | | | ||
| 16 | Transition Systems and Temporal Properties. | |||||
| 17 | Transition Systems and Temporal Properties. Kripke Structures | | | | ||
| 18 | LTL | | | | ||
| 19 | LTL | | | | ||
| 20 | LTL | | | | ||
| 21 | LTL | | | | ||
| 22 | Model Checking | | | | ||
| 23 |
No comments:
Post a Comment