Finite and algorithmic model theory
Finite and algorithmic model theory
Lehrveranstaltung mit SWS 2/2/0 (Vorlesung/Übung/Praktikum) in SS 2021
Dozent
Tutor
Umfang (SWS)
- 2/2/0
Module
Leistungskontrolle
- Mündliche Prüfung
Finite and algorithmic model theory (summer semester 2020/21)
Course Description
The goal of the lecture is to present a basic mathematical tool-kit useful for studying expressivity&complexity of first-order logic and its fragments. It is motivated by applications of logics in computer science (e.g. in formal verification, databases or knowledge representation). The course is recommended to students enjoying theoretical computer science or/and pure mathematics.
The expected content of the lecture will be as follows: 1. Inexperssivity via compactness theorem and why it is not appropriate for finite models. 2. Zero-one laws of FO. 3. Ehrenfeucht-Fraïssé games - a basic tool for showing FO-inexpressivity. 4. FO can express only local properties: Hanf locality with applications to fixed parameter tractability of FO model-checking on graphs of bounded degree. 5. Order-invariant First-Order logic. A few words about the logic for P. 6. On the complexity of fixed-variable fragments of FO. Warm-up: N-completness of FO1 and undecidability of FO3. Solving finite satisfiability for FO1 with counting quantifiers via integer programming. 7. NExpTime-hardness for the two-variable fragment of FO. Playing with binary encodings of numbers and encoding tiles. 8. NExpTime upper bounds for FO2 and its exponential model property. 9. Guarded-Fragment (GF) of First-Order Logic. A recap from alternating Turing machines. Lower bounds. 10. Tree-model property of GF. AExpSpapce=2ExpTime upper bounds. 11. Finite model property for GF, an incomplete but simplified proof of the binary-signature case employing the extension property for partial automorphisms (EPPA, a.k.a. Hrushovski property).
Prerequisites Undergraduate-level knowledge of predicate and first-order logic (syntax&semantics of FO) as well as a little from computational complexity (Turing machines, standard (non)deterministic complexity classes and basic knowledge about undecidable problems) is required.
Schedule and Location Because of the ongoing COVID-19 pandemic, all lectures and tutorials will be online, via Zoom, respectively on Tuesdays (14:50 - 16:20) and Wednesdays (11:10 - 12:40).
The lecturer and the tutor for the course will be Bartosz Bednarczyk, teaching under the supervision of Sebastian Rudolph.- Erich Grädel et al, Finite Model Theory and Its Applications
- Leonid Libkin, Elements of Finite Model Theory
- Martin Otto, Finite Model Theory — Lecture Notes
- Erich Grädel, Algorithmic Model Theory — Lecture Notes
- Erich Gradel, Egon Börger, Yuri Gurevich, The Classical Decision Problem
Veranstaltungskalender abonnieren (icalendar)
| Vorlesung | Introduction & Compactness method | DS5, 13. April 2021 in Videokonferenz | Datei |
| Übung | Q&A | DS3, 14. April 2021 in Videokonferenz | |
| Vorlesung | Zero-One Laws of FO | DS5, 20. April 2021 in Videokonferenz | Datei |
| Übung | Exercises on Compactness | DS3, 21. April 2021 in Videokonferenz | Datei |
| Vorlesung | The missing proofs on 0-1 law + Intro to EF Games | DS5, 27. April 2021 in Videokonferenz | Datei |
| Übung | Exercises on Zero-One Laws | DS3, 28. April 2021 in APB E005 | Datei |
| Vorlesung | E-F Games | DS5, 4. Mai 2021 in APB E005 | Datei |
| Entfällt | NO EXERCISES | DS3, 5. Mai 2021 in APB E005 | |
| Vorlesung | Proving E-F Games | DS5, 11. Mai 2021 in APB E005 | Datei |
| Übung | Exercises on EF games | DS3, 12. Mai 2021 in APB E005 | Datei |
| Vorlesung | Locality | DS5, 18. Mai 2021 in APB E005 | Datei |
| Übung | Exercises on E-F games and locality | DS3, 19. Mai 2021 in APB E005 | Datei |
| Entfällt | No lecture | DS5, 25. Mai 2021 in APB E005 | |
| Entfällt | No exercises | DS3, 26. Mai 2021 in APB E005 | |
| Vorlesung | Tilings and undecidability of FO | DS5, 1. Juni 2021 in APB E005 | Datei |
| Übung | Exercises on pebble games, Hanf locality and MSO | DS3, 2. Juni 2021 in APB E005 | Datei |
| Vorlesung | Model checking on graphs with bounded degree and NP-completeness of FO1 and C1 | DS5, 8. Juni 2021 in APB E005 | Datei |
| Vorlesung | Decidable fragment of first-order logic, C1 and introduction to FO2 | DS5, 15. Juni 2021 in APB E005 | Datei |
| Übung | Exercises on decidability/undecidability | DS3, 16. Juni 2021 in APB E005 | Datei |
| Vorlesung | The last lecture [recap] | DS5, 20. Juni 2021 in APB E005 | |
| Vorlesung | Finite model property for FO2 | DS5, 22. Juni 2021 in APB E005 | Datei |
| Übung | Exercises on C1 and related logics | DS3, 23. Juni 2021 in APB E005 | Datei |
| Vorlesung | Guarded Fragment: Part 1 | DS5, 29. Juni 2021 in APB E005 | Datei |
| Übung | Exercises on FO2 and related logics | DS3, 30. Juni 2021 in APB E005 | |
| Übung | Exercises on FO2 and related logics: Part II | DS3, 7. Juli 2021 in APB E005 | Datei |
| Vorlesung | Guarded Fragment: Part 2 | DS5, 13. Juli 2021 in APB E005 | Datei |
Kalender
