Finite and algorithmic model theory (22/23)
Finite and algorithmic model theory (22/23)
Lehrveranstaltung mit SWS 2/2/0 (Vorlesung/Übung/Praktikum) in WS 2022
Dozent
Tutor
Umfang (SWS)
- 2/2/0
Module
Leistungskontrolle
- Mündliche Prüfung
Finite and algorithmic model theory (summer semester 2022/23)
Course Description
The goal of the lecture is to present a basic mathematical toolkit 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.
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. Don't worry if you are not fluent with the mentioned material from computational complexity -- it will be possible to organize some extra lessons to cover the essentials.
Schedule and Location
In person. Lecture: Wednesdays, 14:50-16:20, APB/E007 Tutorial: Tuesday, 13:00-14:50, BAR/0218 (that's in another building, across the road)
Lecture plan
The expected content of the lecture will be as follows:
1. Inexpressivity 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. On the complexity of fixed-variable fragments of FO, undecidability of FO.
6. NP-completeness of FO1 and solving finite satisfiability for FO1 with counting quantifiers via integer programming.
7. NExpTime upper bounds for FO2 and exponential model property of FO2.
8. ExpTime upper bound for GF2 and its tree-model property.
9. AExpSpapce=2ExpTime upper bounds for full GF.
Opportunities
B. Bednarczyk is happy to provide research-level master's or bachelor's projects ideas (of different difficulty levels) and to supervise them.
Contact
Please, feel free to contact B. Bednarczyk if you have any further questions.- 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, 12. Oktober 2022 in APB/E007 | Datei 1, Datei 2 |
| Vorlesung | Zero-One Laws of FO | DS5, 19. Oktober 2022 in APB/E007 | Datei 1, Datei 2 |
| Übung | Exercise session 1: Compactness | DS4, 20. Oktober 2022 in APB/2026 | Datei |
| Vorlesung | Applying compactness: Preservation theorems. | DS5, 26. Oktober 2022 in APB/E007 | Datei 1, Datei 2 |
| Übung | Exercise session 2: Zero-One Law | DS4, 27. Oktober 2022 in APB/2026 | Datei |
| Vorlesung | Ehrenfeucht–Fraïssé games | DS5, 2. November 2022 in APB/E007 | Datei 1, Datei 2 |
| Übung | Exercise session about alternative definitions of the random graph and Łoś-Tarski theorem. | DS4, 3. November 2022 in APB/2026 | Datei |
| Vorlesung | E-F Games (proofs), Hintikka sets + Locality I: Hanf locality and proof that FO is Hanf-local | DS5, 9. November 2022 in APB/E007 | Datei 1, Datei 2 |
| Übung | Exercise session about E-F Games | DS4, 10. November 2022 in APB/2026 | Datei |
| Entfällt | Day of Prayer and Repentance (NO LECTURE) | DS5, 16. November 2022 in APB/E007 | |
| Entfällt | Day of Prayer and Repentance (NO EXERCISE SESSION) | DS4, 17. November 2022 in APB/2026 | |
| Vorlesung | SAT of FO is undecidable. The quest of finding decidable fragments (survey on recent research trends) | DS1, 23. November 2022 in APB/E007 | |
| Übung | Exercise session about E-F Games, Pebble Games | DS4, 24. November 2022 in APB/2026 | Datei |
| Vorlesung | One variable fragment of FO + NExpTime lower bound for FO2 without equality | DS1, 30. November 2022 in APB/E007 | |
| Übung | Exercise session about ??? | DS4, 1. Dezember 2022 in APB/2026 | |
| Entfällt | One variable fragment with counting quantifiers (Canceled due to sickness) | DS5, 7. Dezember 2022 in APB/E007 | |
| Entfällt | Exercise session about satisfiability (Canceled due to sickness) | DS4, 8. Dezember 2022 in APB/2026 | Datei |
| Entfällt | (Canceled due to sickness) | DS5, 14. Dezember 2022 in APB/E007 | |
| Entfällt | Exercise session about the one-variable fragment of FO and the monadic fragment (Canceled due to sickness) | DS4, 15. Dezember 2022 in APB/2026 | Datei |
| Vorlesung | One variable fragment with counting quantifiers | DS5, 4. Januar 2023 in Videokonferenz | |
| Übung | Exercise session about satisfiability | DS4, 5. Januar 2023 in Videokonferenz | Datei |
| Vorlesung | Finite model property for the two-variable logic | DS5, 11. Januar 2023 in APB/E007 | Datei |
| Übung | Exercise session about the one-variable fragment of FO and the monadic fragment | DS4, 12. Januar 2023 in APB/2026 | Datei |
| Vorlesung | Lecture about the two-variable guarded fragment | DS5, 18. Januar 2023 in Videokonferenz | Datei |
| Entfällt | No exercise session | DS4, 19. Januar 2023 in Videokonferenz | |
| Vorlesung | Lecture about the lower bound for the guarded fragment | DS5, 25. Januar 2023 in APB/E007 | |
| Übung | Exercise session about FO2 | DS4, 26. Januar 2023 in APB/2026 | Datei |
| Vorlesung | Recap lecture + Q&A | DS5, 1. Februar 2023 in APB/E007 | |
| Übung | The last exercise session about ??? | DS4, 2. Februar 2023 in APB/2026 |
Kalender
