Uniwersytet Warszawski - Centralny System Uwierzytelniania
Strona główna

Teoria modeli skończonych

Informacje ogólne

Kod przedmiotu: 1000-2M13TSK
Kod Erasmus / ISCED: 11.3 Kod klasyfikacyjny przedmiotu składa się z trzech do pięciu cyfr, przy czym trzy pierwsze oznaczają klasyfikację dziedziny wg. Listy kodów dziedzin obowiązującej w programie Socrates/Erasmus, czwarta (dotąd na ogół 0) – ewentualne uszczegółowienie informacji o dyscyplinie, piąta – stopień zaawansowania przedmiotu ustalony na podstawie roku studiów, dla którego przedmiot jest przeznaczony. / (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
Przedmioty obieralne na studiach drugiego stopnia na kierunku bioinformatyka
Punkty ECTS i inne: 6.00 Podstawowe informacje o zasadach przyporządkowania punktów ECTS:
  • roczny wymiar godzinowy nakładu pracy studenta konieczny do osiągnięcia zakładanych efektów uczenia się dla danego etapu studiów wynosi 1500-1800 h, co odpowiada 60 ECTS;
  • tygodniowy wymiar godzinowy nakładu pracy studenta wynosi 45 h;
  • 1 punkt ECTS odpowiada 25-30 godzinom pracy studenta potrzebnej do osiągnięcia zakładanych efektów uczenia się;
  • tygodniowy nakład pracy studenta konieczny do osiągnięcia zakładanych efektów uczenia się pozwala uzyskać 1,5 ECTS;
  • nakład pracy potrzebny do zaliczenia przedmiotu, któremu przypisano 3 ECTS, stanowi 10% semestralnego obciążenia studenta.

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 2021/22" (zakończony)

Okres: 2021-10-01 - 2022-02-20
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: Wojciech Czerwiński, 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.
ul. Banacha 2
02-097 Warszawa
tel: +48 22 55 44 214 https://www.mimuw.edu.pl/
kontakt deklaracja dostępności USOSweb 6.8.0.0-2a4334331 (2022-08-26)