Finite Model Theory (January-April 2015)

Pre-requisites

Theory of Computation, Logic

References

  1. Parameterized Complexity Theory by Jörg Flum and Martin Grohe, 2006.
  2. Elements of Finite Model Theory by Leonid Libkin, 2004.
  3. Finite Model Theory by Heinz-Dieter Ebbinghaus and Jörg Flum, 1995

Outline

  1. Graphs and logic: automata and logics, pathwidth, treewidth, Courcelle's theorem, locality of First Order logic, locally bounded treewidth.
  2. EF games: expressive power of FO, MSO.
  3. Turing machines and finite models: Fagin's theorem and NP, ordered structures, fixed point logics, a logic for PTIME?
  4. Zero-one laws.

Homeworks

  1. Homework 1.

Lectures

  1. 6 January: MSO on graphs, statement of Courcelle's theorem, MSO on strings, Büchi, Elgot and Trakhtenbrot Theorem. References: chapters 4.2 and 10.1 of [1].
  2. 8 January: Continuation of BET theorem. Path decompositions and their properties. References: chapters 10.1 and 11.1 of [1].
  3. 13 January: Interpreting a graph on its path decomposition. References: chapter 11.4 of [1].
  4. 20 January: Interpreting a graph on its path decomposition, MSO transductions. References: chapter 11.4 of [1].
  5. 22 January: introduction to tree automata, conclusion of proof of Courcelle's theorem. References: chapters 10.2 and 11.4 of [1].
  6. 27 January: introduction to Ehrenfeucht-Fraïssé games. References: chapters 3.1-3.3 of [2].
  7. 29 January: rank-k m-types. References: chapter 3.4 of [2].
  8. 3 February: proof of Ehrenfeucht-Fraïssé theorem. References: chapter 3.5 of [2].
  9. 5 February: some classical results of First Order logic. References: chapter 0(C) of [3].
  10. 17 February: Gaifman's locality theorem. References: chapter 1 of [3].
  11. 3 March: Model checking first order sentences on classes of graphs with bounded local treewidth. References: chapter 12.2 of [1].
  12. 5 March: Trakhtenbrot's theorem and failure of completeness. References: chapter 9.1 of [2].
  13. 10 March: Fagin's theorem and NP. References: chapter 9.2 of [2].
  14. 12 March: introduction to fixed points of operators on sets. References: chapter 10.1 of [2].
  15. 17 March: fixed point logics. References: chapter 10.2 of [2].
  16. 19 March: simultaneous fixed points. References: chapter 10.3 of [2].
  17. 24 March: LFP captures PTIME on ordered structures. References: chapter 10.4 of [2].
  18. 26 March: Zero-one law for FO on graphs. References: Joshua Horowitz's notes, available here.
  19. 31 March: Zero-one law for LFP on graphs. References: chapters 11.1, 11.2, 12.1 and 12.2 of [2].
  20. 2 April: MSO games and types. References: chapter 7.2 of [2].
  21. 7 April: existential and universal fragments of MSO. References: chapter 7.3 of [2].
  22. 9 April: expressive power of existential MSO, Hanf's locality of FO. References: chapters 7.3, 4.2 and 4.3 of [2].