Account
Edit tools
Intern
SucheSearch
English

Finite and algorithmic model theory (SS2021): Unterschied zwischen den Versionen

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche
(Die Seite wurde neu angelegt: „{{Vorlesung |Title=Finite and algorithmic model theory |Research group=Computational Logic |Lecturers=Bartosz Bednarczyk; Sebastian Rudolph |Tutors=Bartosz Bed…“)
 
Keine Bearbeitungszusammenfassung
 
(76 dazwischenliegende Versionen von 2 Benutzern werden nicht angezeigt)
Zeile 6: Zeile 6:
|Term=SS
|Term=SS
|Year=2021
|Year=2021
|Module=INF-BAS6, INF-VERT6, INF-B-520, INF-PM-FOR, MCL-KR, MCL-PI, MCL-TCSL, CMS-LM-ADV, CMS-LM-MOC
|SWSLecture=2
|SWSLecture=2
|SWSExercise=2
|SWSExercise=2
Zeile 12: Zeile 13:
|Description=Finite and algorithmic model theory (summer semester 2020/21)
|Description=Finite and algorithmic model theory (summer semester 2020/21)


Course Description
===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 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:
The expected content of the lecture will be as follows:
1. Inexperssivity via compactness theorem and why it is not appropriate for finite models.
 
1. Inexpressivity via compactness theorem and why it is not appropriate for finite models.
 
2. Zero-one laws of FO.
2. Zero-one laws of FO.
3. Ehrenfeucht-Fraïssé games - a basic tool for showing FO-inexpressivity.
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
4. FO can express only local properties: Hanf locality with applications to fixed parameter tractability of
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.  
FO model-checking on graphs of bounded degree.


Schedule and Location
5. On the complexity of fixed-variable fragments of FO, undecidability of FO.
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.
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.
|Literature=* Erich Grädel et al, Finite Model Theory and Its Applications
|Literature=* Erich Grädel et al, Finite Model Theory and Its Applications
* Leonid Libkin, Elements of Finite Model Theory
* Leonid Libkin, Elements of Finite Model Theory
Zeile 40: Zeile 59:
* Erich Grädel, Algorithmic Model Theory — Lecture Notes
* Erich Grädel, Algorithmic Model Theory — Lecture Notes
* Erich Gradel, Egon Börger, Yuri Gurevich, The Classical Decision Problem
* Erich Gradel, Egon Börger, Yuri Gurevich, The Classical Decision Problem
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Introduction & Compactness method
|Room=https://tu-dresden.zoom.us/j/84922594756?pwd=RnNrYUNKRkRFTGZZN2NCSjVyMmRqUT09
|Date=2021/04/13
|DS=DS5
|Download=Lecture1-fmt-corrected.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Q&A
|Room=https://zoom.us/j/93512412938?pwd=bW0rclprRUdjT3pEM0VxMzNtM084QT09
|Date=2021/04/14
|DS=DS3
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Zero-One Laws of FO
|Room=https://selfservice.zih.tu-dresden.de/l/link.php?m=109418&p=985722fa
|Date=2021/04/20
|DS=DS5
|Download=Fmt-lecture-2.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Exercises on Compactness
|Room=https://selfservice.zih.tu-dresden.de/l/link.php?m=110253&p=300d88b2
|Date=2021/04/21
|DS=DS3
|Download=FMT exercise list 1.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=The missing proofs on 0-1 law + Intro to EF Games
|Room=https://tu-dresden.zoom.us/j/84922594756?pwd=RnNrYUNKRkRFTGZZN2NCSjVyMmRqUT09
|Date=2021/04/27
|DS=DS5
|Download=FMT-Lecture-3.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Exercises on Zero-One Laws
|Room=APB E005
|Date=2021/04/28
|DS=DS3
|Download=exercise list 2.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=E-F Games
|Room=APB E005
|Date=2021/05/04
|DS=DS5
|Download=FMT-Lecture-4.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Entfällt
|Title=NO EXERCISES
|Room=APB E005
|Date=2021/05/05
|DS=DS3
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Proving E-F Games
|Room=APB E005
|Date=2021/05/11
|DS=DS5
|Download=FMT-Lecture5.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Exercises on EF games
|Room=APB E005
|Date=2021/05/12
|DS=DS3
|Download=Exercise list 3.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Locality
|Room=APB E005
|Date=2021/05/18
|DS=DS5
|Download=FMT-Lecture6.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Exercises on E-F games and locality
|Room=APB E005
|Date=2021/05/19
|DS=DS3
|Download=Exercise list 4.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Entfällt
|Title=No lecture
|Room=APB E005
|Date=2021/05/25
|DS=DS5
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Entfällt
|Title=No exercises
|Room=APB E005
|Date=2021/05/26
|DS=DS3
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Tilings and undecidability of FO
|Room=APB E005
|Date=2021/06/01
|DS=DS5
|Download=FMT-Lecture7.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Exercises on pebble games, Hanf locality and MSO
|Room=APB E005
|Date=2021/06/02
|DS=DS3
|Download=FMT exercise list 5.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Model checking on graphs with bounded degree and  NP-completeness of FO1 and C1
|Room=APB E005
|Date=2021/06/08
|DS=DS5
|Download=FMT-Lecture8.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Decidable fragment of first-order logic, C1 and introduction to FO2
|Room=APB E005
|Date=2021/06/15
|DS=DS5
|Download=FMT-Lecture9.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Exercises on decidability/undecidability
|Room=APB E005
|Date=2021/06/16
|DS=DS3
|Download=FMT exercise list 6.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Finite model property for FO2
|Room=APB E005
|Date=2021/06/22
|DS=DS5
|Download=FMT-Lecture10.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Exercises on C1 and related logics
|Room=APB E005
|Date=2021/06/23
|DS=DS3
|Download=FMT exercise list 7.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Guarded Fragment: Part 1
|Room=APB E005
|Date=2021/06/29
|DS=DS5
|Download=FMT-Lecture11.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Exercises on FO2 and related logics
|Room=APB E005
|Date=2021/06/30
|DS=DS3
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Guarded Fragment: Part 2
|Room=APB E005
|Date=2021/07/13
|DS=DS5
|Download=FMT-Lecture12.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Exercises on FO2 and related logics: Part II
|Room=APB E005
|Date=2021/07/07
|DS=DS3
|Download=Exercise list 8.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=The last lecture [recap]
|Room=APB E005
|Date=2021/06/20
|DS=DS5
}}
}}

Aktuelle Version vom 12. August 2021, 17:30 Uhr

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 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

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

April 2025

MoDiMiDoFrSaSo
31123456
78910111213
14151617181920
21222324252627
2829301234
567891011















Abgerufen von „https://iccl.inf.tu-dresden.de/w/index.php?title=Finite_and_algorithmic_model_theory_(SS2021)&oldid=34533“