Uniwersytet Warszawski - Centralny System UwierzytelnianiaNie jesteś zalogowany | zaloguj się
katalog przedmiotów - pomoc

Teoria modeli skończonych

Informacje ogólne

Kod przedmiotu: 1000-2M13TSK Kod Erasmus / ISCED: 11.3 / (brak danych)
Nazwa przedmiotu: Teoria modeli skończonych
Jednostka: Wydział Matematyki, Informatyki i Mechaniki
Grupy: Przedmioty monograficzne dla III - V roku informatyki
Przedmioty obieralne dla informatyki
Punkty ECTS i inne: 6.00
zobacz reguły punktacji
Język prowadzenia: angielski
Rodzaj przedmiotu:

monograficzne

Założenia (lista przedmiotów):

Złożoność obliczeniowa 1000-218bZO

Skrócony opis:

1.Wyrazistość (6 wykładów)

1.Złożoność ewaluacji logiki pierwszego rzędu

2.Twierdzenie Fagina (NP=ESO)

3.Logiki z punktami stałymi (LFP, IFP, Datalog, TCL)

4.Twierdzenie Immermann-Vardi (PTime=IFP(<))

2.Niewyrażalność (3 wykłady)

1.Gry Ehrenfeucht-Fraisse

2.Lokalność (Gaifman, Hanf)

3.Prawa zero-jedynkowe

3.Zagadnienia z Baz Danych (3 wykłady)

1.problem zawierania zapytań koniunkcyjnych; związek z CSP

2.“Chase”

Pełny opis:

Teoria modeli skończonych to dziedzina informatyki teoretycznej, która łączy aspekty takich dziedzin jak złożoność obliczeniowa, teoria baz danych i logika.

Związek ze złożonością obliczeniową polega na obserwacji, że wiele klas złożoności (takich jak LogSpace, P, NP itd.) można scharakteryzować za pomocą rozmaitych logik.

Dla przykładu, dla każdej wielomianowej (należącej do P) własności grafowej W istnieje równoważna formuła φ logiki pierwszego rzędu rozszerzonej o operację brania punktów stałych. Równoważność ta oznacza, że dla każdego grafu uporządkowanego (G,<), graf G ma własność W wtedy i tylko wtedy, gdy spełnia formułę φ. Jednym z zagadnień badanych na tym przedmiocie są logiczne charakteryzacje wielu klas złożoności.

Powyższe związki prowadzą natychmiast do pytania, jak rozróżniać siłę wyrazu różnych logik. Będziemy badać różne narzędzia do tego służące: gry Ehrenfeuchta-Fraisse, prawa zero-jedynkowe, twierdzenia o lokalności.

Związek z teorią baz danych jest bardzo bliski: model skończony jest matematyczną formalizacją pojęcia ,,baza danych”. Zapytania do bazy danych w danym języku (np. SQL) można postrzegać jako ewaluację formuł odpowiedniej logiki na danym modelu. Dlatego wiele pytań z teorii baz danych (np. złożoność ewaluacji danej formuły, pytanie o spełnialność formuły, itd.) są de facto pytaniami z teorii modeli skończonych. Na tym przedmiocie będziemy również rozważać takie pytania.

Literatura:

- Notatki do wykładu, http://duch.mimuw.edu.pl/~szymtor/wordpress/?cat=6

- Leonid Libkin, Elements of Finite Model Theory;

- Erich Graedel, Finite Model Theory;

- Serge Abiteboul, Richard Hull, Victor Vianu, Foundations of Databases;

- Neil Immerman, Descriptive Complexity;

- Ronald Fagin, Finite Model Theory – A personal perspective;

- Phokion G. Kolaitis, Reflections on Finite Model Theory;

- Martin Grohe, Descriptive Complexity;

- Jouko Väänänen, A Short Course on Finite Model Theory;

- Erich Gradel, Algorithmic Model Theory

Efekty uczenia się:

Rozumie związki pomiędzy złożnością obliczeniową problemu, a logiką, w jakiej dany problem da się wyrazić.

Metody i kryteria oceniania:

Ocena końcowa na podstawie zadań domowych oraz oceny z egzaminu ustnego

Zajęcia w cyklu "Semestr zimowy 2020/21" (jeszcze nie rozpoczęty)

Okres: 2020-10-15 - 2021-01-31
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Ćwiczenia, 30 godzin więcej informacji
Wykład, 30 godzin więcej informacji
Koordynatorzy: Szymon Toruńczyk
Prowadzący grup: Szymon Toruńczyk
Lista studentów: (nie masz dostępu)
Zaliczenie: Egzamin
Opisy przedmiotów w USOS i USOSweb są chronione prawem autorskim.
Właścicielem praw autorskich jest Uniwersytet Warszawski.