Finite and algorithmic model theory

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche

Finite and algorithmic model theory

Lehrveranstaltung mit SWS 2/2/0 (Vorlesung/Übung/Praktikum) in SS 2021

Finite and algorithmic model theory (summer semester 2020/21)

Please register to OPAL's course webpage: https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/29952770050?0

Zoom links are "Termine und Unterlagen" section.

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. Order-invariant First-Order logic. A few words about a logic for PTime.

6. On the complexity of fixed-variable fragments of FO. Warm-up: NP-completeness of FO1 and undecidability of FO3. Solving finite satisfiability for FO1 with counting quantifiers via integer programming.

7. NExpTime-hardness of 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 for the binary-signature case, employing the extension property for partial automorphisms (EPPA, a.k.a. Hrushovski property).

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 DS1, 13. April 2021 in Videokonferenz Datei
Übung Q&A DS1, 14. April 2021 in APB E005
Vorlesung Zero-One Laws of FO DS1, 20. April 2021 in APB E005
Übung Exercises on Compactness DS1, 21. April 2021 in APB E005 Datei
Vorlesung E-F Games Part 1 DS1, 27. April 2021 in APB E005
Übung Exercises on Zero-One Laws DS1, 28. April 2021 in APB E005
Vorlesung E-F Games Part 2 DS1, 4. Mai 2021 in APB E005
Übung Exercises on E-F Games DS1, 5. Mai 2021 in APB E005
Vorlesung Locality: Part 1 DS1, 11. Mai 2021 in APB E005
Vorlesung Locality: Part 2 DS1, 12. Mai 2021 in APB E005
Vorlesung Order-Invariant FO DS1, 18. Mai 2021 in APB E005
Übung Exercises on locality DS1, 19. Mai 2021 in APB E005
Vorlesung Tilings and undecidability of FO DS1, 25. Mai 2021 in APB E005
Übung Exercises on locality DS1, 26. Mai 2021 in APB E005


Kalender