Account
Edit tools
Intern
SucheSearch
English

Finite and algorithmic model theory (22/23) (WS2022): 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 (22/23) |Research group=Computational Logic |Lecturers=Bartosz Bednarczyk; Sebastian Rudolph |Tutors=Bar…“)
 
Keine Bearbeitungszusammenfassung
 
(64 dazwischenliegende Versionen desselben Benutzers werden nicht angezeigt)
Zeile 6: Zeile 6:
|Term=WS
|Term=WS
|Year=2022
|Year=2022
|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
|SWSPractical=0
|SWSPractical=0
|Exam type=mündliche Prüfung
|Exam type=mündliche Prüfung
|Description=Finite and algorithmic model theory (summer semester 2022/23)
|Description=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===
===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.
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.


===Prerequisites===
===Schedule and Location===


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


===Schedule and Location===
Lecture: Wednesdays, 14:50-16:20,  APB/E007


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).
Tutorial: Thursday, 13:00-14:50, APB/2026.
The lecturer and the tutor for the course will be Bartosz Bednarczyk, teaching under the supervision of Sebastian Rudolph.


===Lecture plan===
===Lecture plan===
Zeile 29: Zeile 36:
The expected content of the lecture will be as follows:
The expected content of the lecture will be as follows:


1. Inexpressivity 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. 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.
2. Zero-one laws of FO.
Zeile 38: Zeile 45:
FO model-checking on graphs of bounded degree.
FO model-checking on graphs of bounded degree.


5. On the complexity of fixed-variable fragments of FO, undecidability of FO.
5. A bit of model theory for the modal logic K.
 
6. Order-invariant First-Order Logic.


6. NP-completeness of FO1 and solving finite satisfiability for FO1 with counting quantifiers via integer programming.
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).


7. NExpTime upper bounds for FO2 and exponential model property of FO2.
8. The two-variable fragment of FO, model theory, complexity and the finite model property.


8. ExpTime upper bound for GF2 and its tree-model property.
9. The guarded fragment of FO, model theory, complexity and the finite model property.


9. AExpSpapce=2ExpTime upper bounds for full GF.


===Opportunities===
===Opportunities===
B. Bednarczyk is happy to provide research-level master's or bachelor's projects ideas (of different difficulty levels) and to supervise them.
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===
===Contact===
Please, feel free to contact B. Bednarczyk if you have any further questions.
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!
|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 58: Zeile 70:
* 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=APB/E007
|Date=2022/10/12
|DS=DS5
|Download=FaAMT-Lecture1-Long-Corrected-20-10-22.pdf,FaAMT-Lecture1-Short-Corrected-20-10-22.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Zero-One Laws of FO
|Room=APB/E007
|Date=2022/10/19
|DS=DS5
|Download=FaAMT-Lecture2-Short.pdf,FaAMT-Lecture2-Long.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Applying compactness: Preservation theorems.
|Room=APB/E007
|Date=2022/10/26
|DS=DS5
|Download=FaAMT-Lecture3-Long-Corrected-29-10-22.pdf,FaAMT-Lecture3-Short-Corrected-29-10-22.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Ehrenfeucht–Fraïssé games
|Room=APB/E007
|Date=2022/11/02
|DS=DS5
|Download=FaAMT-Lecture4-Long.pdf,FaAMT-Lecture4-Short.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=E-F Games (proofs), Hintikka sets + Locality I: Hanf locality and proof that FO is Hanf-local
|Room=APB/E007
|Date=2022/11/09
|DS=DS5
|Download=FaAMT-Lecture5-Long.pdf,FaAMT-Lecture5-Short.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=SAT of FO is undecidable. The quest of finding decidable fragments (survey on recent research trends)
|Room=APB/E007
|Date=2022/11/23
|DS=DS1
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=One variable fragment of FO + NExpTime lower bound for FO2 without equality
|Room=APB/E007
|Date=2022/11/30
|DS=DS1
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Entfällt
|Title=One variable fragment with counting quantifiers (Canceled due to sickness)
|Room=APB/E007
|Date=2022/12/07
|DS=DS5
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Entfällt
|Title=(Canceled due to sickness)
|Room=APB/E007
|Date=2022/12/14
|DS=DS5
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=One variable fragment with counting quantifiers
|Room=https://tu-dresden.zoom.us/j/84922594756?pwd=RnNrYUNKRkRFTGZZN2NCSjVyMmRqUT09#success
|Date=2023/01/04
|DS=DS5
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Finite model property for the two-variable logic
|Room=APB/E007
|Date=2023/01/11
|DS=DS5
|Download=FMT-lecture-FO2.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Lecture about the two-variable guarded fragment
|Room=https://tu-dresden.zoom.us/j/84922594756?pwd=RnNrYUNKRkRFTGZZN2NCSjVyMmRqUT09#success
|Date=2023/01/18
|DS=DS5
|Download=FMT-LEcture-8.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Lecture about the lower bound for the guarded fragment
|Room=APB/E007
|Date=2023/01/25
|DS=DS5
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Recap lecture + Q&A
|Room=APB/E007
|Date=2023/02/01
|DS=DS5
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Entfällt
|Title=Day of Prayer and Repentance (NO LECTURE)
|Room=APB/E007
|Date=2022/11/16
|DS=DS5
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Exercise session 1: Compactness
|Room=APB/2026
|Date=2022/10/20
|DS=DS4
|Download=BBE-FMT-Exercises1.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Exercise session 2: Zero-One Law
|Room=APB/2026
|Date=2022/10/27
|DS=DS4
|Download=FaAMT-Exercises2.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Exercise session about alternative definitions of the random graph and Łoś-Tarski theorem.
|Room=APB/2026
|Date=2022/11/03
|DS=DS4
|Download=FaAMT-Exercises3.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Exercise session about E-F Games
|Room=APB/2026
|Date=2022/11/10
|DS=DS4
|Download=FaAMT-Exercises4.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Entfällt
|Title=Day of Prayer and Repentance (NO EXERCISE SESSION)
|Room=APB/2026
|Date=2022/11/17
|DS=DS4
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Exercise session about E-F Games, Pebble Games
|Room=APB/2026
|Date=2022/11/24
|DS=DS4
|Download=FaAMT-Exercises5.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Exercise session about ???
|Room=APB/2026
|Date=2022/12/01
|DS=DS4
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Entfällt
|Title=Exercise session about satisfiability  (Canceled due to sickness)
|Room=APB/2026
|Date=2022/12/08
|DS=DS4
|Download=FMT exercise list 6 new.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Entfällt
|Title=Exercise session about the one-variable fragment of FO and the monadic fragment (Canceled due to sickness)
|Room=APB/2026
|Date=2022/12/15
|DS=DS4
|Download=FMT exercise list 7.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Exercise session about the one-variable fragment of FO and the monadic fragment
|Room=APB/2026
|Date=2023/01/12
|DS=DS4
|Download=FMT exercise list 7.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Entfällt
|Title=No exercise session
|Room=https://tu-dresden.zoom.us/j/84922594756?pwd=RnNrYUNKRkRFTGZZN2NCSjVyMmRqUT09#success
|Date=2023/01/19
|DS=DS4
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Exercise session about FO2
|Room=APB/2026
|Date=2023/01/26
|DS=DS4
|Download=Fmt exercises.pdf,
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=The last exercise session about ???
|Room=APB/2026
|Date=2023/02/02
|DS=DS4
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Exercise session about satisfiability
|Room=https://tu-dresden.zoom.us/j/84922594756?pwd=RnNrYUNKRkRFTGZZN2NCSjVyMmRqUT09#success
|Date=2023/01/05
|DS=DS4
|Download=FMT exercise list 6 new.pdf
}}
}}

Aktuelle Version vom 23. Januar 2023, 14:59 Uhr

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


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

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
















Abgerufen von „https://iccl.inf.tu-dresden.de/w/index.php?title=Finite_and_algorithmic_model_theory_(22/23)_(WS2022)&oldid=37797“