Finite and algorithmic model theory (22/23)
Finite and algorithmic model theory (22/23)
Course with SWS 2/2/0 (lecture/exercise/practical) in WS 2022
Lecturer
Tutor
SWS
- 2/2/0
Modules
Examination method
- Oral exam
Check the newest lecture slides and exercise lists! OPAL: https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/37215338499
Finite and algorithmic model theory (winter semester 2022/23). The lectures and exercise sessions will be given by Bartosz Bednarczyk.
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. Note that the course is intended to be relatively advanced.
Schedule and Location
In-person, blackboard talk (with slides from time to time). Both lectures and exercise sessions will be given by Bartosz Bednarczyk. Exercise sessions will contain material required for the lecture and vice-versa, so I fully recommend attending the exercise sessions (or at list skimming the exercise list before attending the lecture).
Lecture: Wednesdays, 14:50-16:20, APB/E007
Tutorial: Thursday, 13:00-14:50, APB/2026.
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. Applications of compactness in proving useful model-theoretic properties of FO like interpolation, preservation theorems and so on. Failures of such properties in the finite.
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. A bit of model theory for the modal logic K.
6. Order-invariant First-Order Logic.
7. Undecidability of the satisfiability problem for FO and related issues. NP-completeness of FO1 and solving finite satisfiability for FO1 with counting quantifiers (a detour through integer programming).
8. The two-variable fragment of FO, model theory, complexity and the finite model property.
9. The guarded fragment of FO, model theory, complexity and the finite model property.
Opportunities
B. Bednarczyk is happy to provide research-level master's or bachelor's project ideas (of different difficulty levels) and to supervise them. There is a very high chance to offer scholarships to students interested in doing research.
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 and such notions are not required for 80% of the lecture.
Contact
Please, feel free to contact B. Bednarczyk via email (bartosz.bednarczyk at cs.uni.wroc.pl) if you have any further questions. I promise to reply no later than after 10 hours!- 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, October 12, 2022 in APB/E007 | File 1, File 2 |
| Lecture | Zero-One Laws of FO | DS5, October 19, 2022 in APB/E007 | File 1, File 2 |
| Exercise | Exercise session 1: Compactness | DS4, October 20, 2022 in APB/2026 | File |
| Lecture | Applying compactness: Preservation theorems. | DS5, October 26, 2022 in APB/E007 | File 1, File 2 |
| Exercise | Exercise session 2: Zero-One Law | DS4, October 27, 2022 in APB/2026 | File |
| Lecture | Ehrenfeucht–Fraïssé games | DS5, November 2, 2022 in APB/E007 | File 1, File 2 |
| Exercise | Exercise session about alternative definitions of the random graph and Łoś-Tarski theorem. | DS4, November 3, 2022 in APB/2026 | File |
| Lecture | E-F Games (proofs), Hintikka sets + Locality I: Hanf locality and proof that FO is Hanf-local | DS5, November 9, 2022 in APB/E007 | File 1, File 2 |
| Exercise | Exercise session about E-F Games | DS4, November 10, 2022 in APB/2026 | File |
| No session | Day of Prayer and Repentance (NO LECTURE) | DS5, November 16, 2022 in APB/E007 | |
| No session | Day of Prayer and Repentance (NO EXERCISE SESSION) | DS4, November 17, 2022 in APB/2026 | |
| Lecture | SAT of FO is undecidable. The quest of finding decidable fragments (survey on recent research trends) | DS1, November 23, 2022 in APB/E007 | |
| Exercise | Exercise session about E-F Games, Pebble Games | DS4, November 24, 2022 in APB/2026 | File |
| Lecture | One variable fragment of FO + NExpTime lower bound for FO2 without equality | DS1, November 30, 2022 in APB/E007 | |
| Exercise | Exercise session about ??? | DS4, December 1, 2022 in APB/2026 | |
| No session | One variable fragment with counting quantifiers (Canceled due to sickness) | DS5, December 7, 2022 in APB/E007 | |
| No session | Exercise session about satisfiability (Canceled due to sickness) | DS4, December 8, 2022 in APB/2026 | File |
| No session | (Canceled due to sickness) | DS5, December 14, 2022 in APB/E007 | |
| No session | Exercise session about the one-variable fragment of FO and the monadic fragment (Canceled due to sickness) | DS4, December 15, 2022 in APB/2026 | File |
| Lecture | One variable fragment with counting quantifiers | DS5, January 4, 2023 in Video conference | |
| Exercise | Exercise session about satisfiability | DS4, January 5, 2023 in Video conference | File |
| Lecture | Finite model property for the two-variable logic | DS5, January 11, 2023 in APB/E007 | File |
| Exercise | Exercise session about the one-variable fragment of FO and the monadic fragment | DS4, January 12, 2023 in APB/2026 | File |
| Lecture | Lecture about the two-variable guarded fragment | DS5, January 18, 2023 in Video conference | File |
| No session | No exercise session | DS4, January 19, 2023 in Video conference | |
| Lecture | Lecture about the lower bound for the guarded fragment | DS5, January 25, 2023 in APB/E007 | |
| Exercise | Exercise session about FO2 | DS4, January 26, 2023 in APB/2026 | File |
| Lecture | Recap lecture + Q&A | DS5, February 1, 2023 in APB/E007 | |
| Exercise | The last exercise session about ??? | DS4, February 2, 2023 in APB/2026 |
Calendar
