Lec# | Topic | Slides PDF/PPT |
1 | Course overview and logistics; A brief history of logic | |
2 | Propositional logic -- syntax and semantics; Konig's Lemma | Lecture #2 - Slides (PDF) Printable (PDF) |
3 | Proof systems for propositional logic: Resolution proof system, A Hilbert/Frege style proof system, Soundness of these systems | Lecture #3 - Slides (PDF) Printable (PDF) |
4 | Propositional logic: Hintikka's lemma, Model-existence theorem | Lecture #4 - Slides (PDF) Printable (PDF) |
5 | Compactness theorem: Two proofs: One using Model-existence theorem; one using Konig's lemma. | Lecture# 5: Lost due to computer crash! |
6 | Propositional Consequence/Strong Completeness Theorem for Resolution. The Advent of SAT solver technology: history, DPLL, conflict clause learning, and modern SAT solvers. | Lecture #6: Strong Completeness: Slides (PDF) Printable (PDF) |
7 | Review of automata theory, computability and complexity theory. Cook-Levin theorem (SAT is NP-complete) and its proof. | Lecture #7: Review of automata, computability and complexity (Mahesh's notes): Slides (PDF) Printable (PDF) Cook-Levin Theorem and some interesting complexity theory results: Slides (PDF) Printable (PDF) |
8 | First-order logic: Syntax and semantics; Equality | Lecture #8: Slides (PDF) Printable (PDF) |
9 10 | First Order Logic: Hintikka's Lemma Model-existence Theorem Resolution: Soundness & Completeness | Lectures #9 and #10: Slides (PDF) Printable (PDF) |
11 | Church-Turing Theorem: Validity of FOL is undecidable. Godel's incompleteness theorem (first) | Lecture #11: Slides (PDF) Printable (PDF) |
12 13 | Second-order logics Monadic second-order logics MSO over words and Regular Languages | Lecture #12 and #13: Slides (PDF) |
14 | Interpretations: Deciding FOL(N,+,0,1) by interpretation on MSO(N, succ). Deciding FOL over infinite trees by interpretation on MSO(N, succ) | Lecture #14: Slides (PDF) |
15 | Monadic Second Order Logic on finite trees MSO and regular tree languages MSO on infinite trees; Rabin's theorem: MSO over infinite trees is decidable | Lecture #15: Slides (PDF) |
16 | Decidability of emptiness of tree automata; solving finite-state games; brief sketch of checking emptiness of automata on infinite trees. | Lecture #16: Slides (PDF) |
17 | MSO interpretations: Decidability of MSO on n-ary trees; Decidability of MSO on series-parallel graphs. | Lecture #17: Slides (PDF) |
18 | More interpretations: Decidability of MSO on pushdown graphs Decidability of FO on automatic graphs (part 1) | Lecture #18: Slides (PDF) |
19 | Decidability of FO on automatic graphs (part II) FO of reals with addition and multiplication is decidable (Tarski) Quantifier elimination | Lecture #19: Slides (PDF) |
20 | Finite model theory I: Review of classical logic. Failiure of fundamental theorems in finite model theory: compactness theorem fails, valid sentences not in r.e. (Trakhtenbrot's theorem) The three themes: 1. Logic and compexity theory 2. (In)expressivess of logics, EF games 3. Classical theorems reevaluated in the finite model setting. | Lecture #20: Slides (PDF) |
21 22 | Finite model theory: Ehrenfeucht-Fraisse Games Quantifier rank EVEN not expressible in FOL CONNECTED not expressible in FOL Proof of EF-theorem; Rank-k types | Lecture #21 & #22: Slides (PDF) |
23 | Finite model theory: - Fagin's theorem ESO=NP | Lecture #23: Slides (PDF) |
24 | Finite model theory: - Fagin's theorem continued - Fixed point logics * Monotonic & inflationary operators * FO + LFP | Lecture #24: Slides (PDF) |
25 | Finite model theory (concluding) - FO+LFP = P (no proof) - FO+PFP = PSPACE (no proof) - EMSO notequals AMSO on structures (no proof) Courcelle's theorem: - Embedding graphs in trees (examples) - Definition of tree-width | Lecture #25: Slides (PDF) |
26 | Fixed-parameter tractability Courcelle's theorem - Any MSO property on finite graphs of bounded tree-width can be model-checked in linear time. | Lecture #26: Slides (PDF) |
FALL BREAK - NO CLASS | ||
FALL BREAK - NO CLASS | ||
27, 28 | Review of topics and results; Also SMT solvers | Lecture #27, Lecture #28 Slides (PDF) |
Logic in Computer Science
Subscribe to:
Post Comments (Atom)
No comments:
Post a Comment