Logo ČVUT
Loading...
CZECH TECHNICAL UNIVERSITY IN PRAGUE
STUDY PLANS
2023/2024
Faculties | School elective courses | ECTS courses catalogue | Settings | Česká verze
Welcome page > Faculty of Information Technology > Department of Theoretical Computer Science > Finite model theory

Finite model theory

Login to KOS for course enrollment Display time-table
Code Completion Credits Range
NI-FMT Z,ZK 4 2P+1C
Garant předmětu:
Tomáš Jakl
Lecturer:
Tomáš Jakl
Tutor:
Tomáš Jakl
Supervisor:
Department of Theoretical Computer Science
Synopsis:

The aim of the course is to introduce students to the basics of finite model theory. The original motivation is the questions expressibility and verifiability of logical properties of database systems. Since its inception in the 1970s, the course has evolved rapidly and touched on many other areas of theoretical computer science, such as descriptive complexity theory, the Constraint Satisfaction Problem (CSP), the theory of algorithmic meta-theorems and combinatorics.

Requirements:

The student is assumed to be familiar with standard basic courses of theoretical computer science at FIT CTU such as discrete mathematics and logic (BIE-DML) and graphs and algorithms (BIE-AG1).

Syllabus of lectures:

1. Course overview, motivation and relation to the theory of database systems [L][FE][G&al]

We review the basics of mathematical logic and its relationship to expressing properties of graphs and relational structures and explain how database systems can be described as finite relational structures. We also explain the limitations of logic on finite structures.

2. Ehrenfeucht-Fraı̈ssé games [L, Chapter 3]

We introduce the Ehrenfeucht-Fraı̈ssé (E-F) games as one of the basic tools of model theory. As an

example, we also discuss the problem of isomorphism and logical equivalence of two finite structures.

Next, we show the first restriction, on the number of rounds, which identifies a fragment of the first-order

logic on formulas of bounded quantifier depth.

3. Inexpressibility theorems in first-order logic [L, Ch. 3].

An important application of the E-F games is in showing whether a given property of graphs or relational structures is expressible in first-order logic. We explain and demonstrate this technique with examples.

As a motivating example we show that connectedness is not expressible in first-order logic.

4. Hanf's locality theorem [FE, ch. 2]

We state and prove Hanf's locality theorem and its threshold variant, the Fagin-Stockmeyer-Vardi theorem. We will show that the inexpressibility of connectedness also a direct consequence of this theorem, and we will add other consequences of inexpressibility, such as parity.

5. Gaifman's locality theorem [FE, ch. 2]

To motivate Gaifman's theorem, we show examples where we cannot make use of Hanf's theorem.

We introduce the construction of a Gaifman graph to a given relational structure and prove Gaifman's theorem.

As an application, we show the Ajtai-Gurevich theorem.

6. Descriptive complexity and second-order logic [L, Ch. 6,9]

We explain the relationship between logic and computational complexity. We discuss the relationship of first-order logic and the computational class PTIME. Next, we state Fagin's theorem, expressing that the existential second-order logic corresponds to a complexity class NP. We also mention the extension of first-order logic to fixpoint operators and the corresponding computational complexity.

7. Logics with the ability to calculate [L, ch. 8]

We introduce the bijective E-F games and extend first-order logic with quantifiers expressing the number of satisfiable assignments, and prove the relation between the winning strategy in the bijective E-F game and the corresponding logical equivalence. We analyze the algorithmic power of counting quantifiers.

8. Turing machines and finite models [L, Ch. 9].

We prove Trakhtenbrot's theorem and the failure of compactness on finite models. We also discuss other theorems from infinite model theory and their restrictions to finite structures. The main positive example will be Rossman's Homomorphism Preservation Theorem.

9. Logics with a finite number of variables [L, Ch. 11]

We introduce pebble games and show their correspondence with fragments of logics with a restricted number of variables. We will discuss the connection with the extension to counting quantifiers. Finally, we show that, despite the inability to express connectedness, the (logical) logical theory of a structure can help to identify connectedness or different types of disconnectedness.

10. Constraints satisfaction problem and logic [G&al, ch. 6].

We explain the relation between the Constraints Satisfaction Problem and the problem of existence of homomorphisms. Using the Chandra-Merlin correspondence, we translate this problem into the language of existencial-positive logic. We show how the syntactic restrictions on the number of variables and quantifier depth correspond to tree-width and tree-depth.

11. Game comonads and one-way games [AS][ADW]

We introduce one-way games and show their correspondence with existencial-positive fragments. We motivate comonads as encodings of one-way E-F and pebble games. We show that such encodings satisfy the axioms of comonads.

12. Coalgebras of game comonads [AS][ADW]

We introduce the notion of coalgebras and explain the relationship of coalgebras of our comonads to the combinatorial properties of treewidth and depth.

13. Game Comonads and Logic [AS][ADW]

We will uniformly describe bijective and classical forms of E-F and pebble games in the category of coalgebras for our game comonads. As an application, we prove some basic theorems from logic using comonads, i.e. without having to work with the syntactic description of the logic in question.

Syllabus of tutorials:

1. Exercises from Ehrenfeucht-Fraı̈ssé games for deciding or disproving logical equivalence.

2. Consultation on the term paper, determination of the topic of the paper.

3. Exercises on locality theorems as a tool for proving winning strategies of the Duplicator in E-F games.

4. Consultation on the term paper, focusing on discussion of the assigned literature.

5. Exercises on variants of E-F games and especially their relation to different fragments of first-order logic.

6. Consultation on the term paper, discussion of the content of the text.

7. Exercises on game comonads + credit test

Study Objective:
Study materials:

[L] Leonid Libkin. Elements of Finite Model Theory. Springer-Verlag 2004.

[FE] Heinz-Dieter Ebbinghaus, Jörg Flum. Finite Model Theory: Second Edition. Springer-Verlag 1995.

[T] Szymon Toruńczyk. Lectures on Finite Model Theory, University of Warsaw, 2022.

https://duch.mimuw.edu.pl/~szymtor/fmt.pdf

[G&al] Erich Gradel, Phokion Kolaitis, Leonid Libkin, Maarten Marx, Joel Spencer, Moshe Y Vardi,

Yde Venema, Scott Weinstein. Finite Model Theory and Its Applications. Springer-Verlag 2007.

[AS] Samson Abramsky, Nihil Shah. Relating Structure and Power, Comonadic Semantics for

Computational Resources. Journal of Logic and Computation, 2021.

[ADW] Samson Abramsky, Anuj Dawar, Pengming Wang. The pebbling comonad in Finite Model

Theory. 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) 2017.

Note:
Further information:
https://courses.fit.cvut.cz/NI-FMT
Time-table for winter semester 2023/2024:
Time-table is not available yet
Time-table for summer semester 2023/2024:
06:00–08:0008:00–10:0010:00–12:0012:00–14:0014:00–16:0016:00–18:0018:00–20:0020:00–22:0022:00–24:00
Mon
Tue
Wed
roomT9:346
Jakl T.
09:15–10:45
(lecture parallel1)
Dejvice
NBFIT uččebnaroomT9:346
Jakl T.
11:00–11:45
(lecture parallel1
parallel nr.101)
Dejvice
NBFIT uččebna
Thu
Fri
The course is a part of the following study plans:
Data valid to 2024-04-26
Copyright © Jiří Kosek, 2010–2022 | Copyright © ČVUT, 2010–2022
Hosted by Výpočetní a informační centrum ČVUT
Send your questions and comments to HelpDesk ČVUT or to spravcekos@cvut.cz
Aktualizace výše uvedených informací naleznete na adrese https://bilakniha.cvut.cz/en/predmet7784906.html