Finite and algorithmic model theory
Finite and algorithmic model theory
Course with SWS 2/2/0 (lecture/exercise/practical) in SS 2021
Lecturer
Tutor
SWS
- 2/2/0
Modules
Examination method
- Oral exam
Finite and algorithmic model theory (summer semester 2020/21)
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
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.
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
Subscribe to events of this course (icalendar)
| Lecture | Introduction & Compactness method | DS5, April 13, 2021 in Video conference | File |
| Exercise | Q&A | DS3, April 14, 2021 in Video conference | |
| Lecture | Zero-One Laws of FO | DS5, April 20, 2021 in Video conference | File |
| Exercise | Exercises on Compactness | DS3, April 21, 2021 in Video conference | File |
| Lecture | The missing proofs on 0-1 law + Intro to EF Games | DS5, April 27, 2021 in Video conference | File |
| Exercise | Exercises on Zero-One Laws | DS3, April 28, 2021 in APB E005 | File |
| Lecture | E-F Games | DS5, May 4, 2021 in APB E005 | File |
| No session | NO EXERCISES | DS3, May 5, 2021 in APB E005 | |
| Lecture | Proving E-F Games | DS5, May 11, 2021 in APB E005 | File |
| Exercise | Exercises on EF games | DS3, May 12, 2021 in APB E005 | File |
| Lecture | Locality | DS5, May 18, 2021 in APB E005 | File |
| Exercise | Exercises on E-F games and locality | DS3, May 19, 2021 in APB E005 | File |
| No session | No lecture | DS5, May 25, 2021 in APB E005 | |
| No session | No exercises | DS3, May 26, 2021 in APB E005 | |
| Lecture | Tilings and undecidability of FO | DS5, June 1, 2021 in APB E005 | File |
| Exercise | Exercises on pebble games, Hanf locality and MSO | DS3, June 2, 2021 in APB E005 | File |
| Lecture | Model checking on graphs with bounded degree and NP-completeness of FO1 and C1 | DS5, June 8, 2021 in APB E005 | File |
| Lecture | Decidable fragment of first-order logic, C1 and introduction to FO2 | DS5, June 15, 2021 in APB E005 | File |
| Exercise | Exercises on decidability/undecidability | DS3, June 16, 2021 in APB E005 | File |
| Lecture | The last lecture [recap] | DS5, June 20, 2021 in APB E005 | |
| Lecture | Finite model property for FO2 | DS5, June 22, 2021 in APB E005 | File |
| Exercise | Exercises on C1 and related logics | DS3, June 23, 2021 in APB E005 | File |
| Lecture | Guarded Fragment: Part 1 | DS5, June 29, 2021 in APB E005 | File |
| Exercise | Exercises on FO2 and related logics | DS3, June 30, 2021 in APB E005 | |
| Exercise | Exercises on FO2 and related logics: Part II | DS3, July 7, 2021 in APB E005 | File |
| Lecture | Guarded Fragment: Part 2 | DS5, July 13, 2021 in APB E005 | File |
Calendar
