Uniwersytet Jagielloński w Krakowie - Punkt LogowaniaNie jesteś zalogowany | zaloguj się
katalog przedmiotów - pomoc

Finite Model Theory

Informacje ogólne

Kod przedmiotu: WMI.TCS.FMT.S Kod Erasmus / ISCED: (brak danych) / (0588) Interdyscyplinarne programy i kwalifikacje obejmujące nauki przyrodnicze, matematykę i statystykę
Nazwa przedmiotu: Finite Model Theory
Jednostka: Instytut Informatyki Analitycznej
Grupy:
Punkty ECTS i inne: 6.00
zobacz reguły punktacji
Język prowadzenia: angielski

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

Okres: 2020-10-01 - 2021-01-28

Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Ćwiczenia, 30 godzin więcej informacji
Wykład, 30 godzin więcej informacji
Koordynatorzy: Michał Wrona
Prowadzący grup: Michał Wrona
Lista studentów: (nie masz dostępu)
Zaliczenie: Przedmiot - Egzamin
Efekty kształcenia:

Student:


-- zna formalne modele obliczeń, bariery obliczalności, trudności obliczeń i ich znaczenie w praktycznych zastosowaniach (K_W05) ,


-- zna zaawansowane techniki analizy i modelowania

problemów informatycznych (K_W06) ,


-- na współczesne kierunki rozwoju i osiągnięcia nauki

w wybranych dziedzinach informatyki (K_W12),


-- potrafi konstruować modele matematyczne dla problemów obliczeniowych (K_U02),


-- rozróżnia deterministyczne i niedeterministyczne kl

asy złożoności obliczeniowej (K_U06).

Wymagania wstępne:

Podstawowa wiedza z logiki, języków formalnych oraz złożoności obliczeniowej.

Forma i warunki zaliczenia:

Student otrzymuję ocenę na podstawie aktywności na zajęciach (liczby otrzymanych punktów) oraz (opcjonalnie) egzaminu.


Aby otrzymać ocenę 3.0, 3.5, 4.0, 4.5, 5.0 należy zdobyć odpowiednio 7,8,9,10 lub 11 punktów. Z egzaminu można uzyskać co najwyżej 5 punktów.

Metody sprawdzania i kryteria oceny efektów kształcenia uzyskanych przez studentów:

Rozwiązywanie zadań na tablicy. Egzamin.

Metody dydaktyczne - słownik:

Metody podające - prelekcja
Metody podające - prezentacja multimedialna
Metody podające - wykład informacyjny
Metody praktyczne - ćwiczenia przedmiotowe

Metody dydaktyczne:

Wykład (z użyciem prezentacji komputerowej oraz tablicy) oraz ćwiczenia na których student pod okiem prowadzącego rozwiązuje zadania na tablicy.

Bilans punktów ECTS:

6 ECTS

Pełny opis:

Teoria modeli to dziedzina logiki matematycznej, która bada zależności pomiędzy językami formalnymi (logikami) oraz strukturami (modelami).

Teoria modeli skończonych to część teorii modeli ukierunkowana na zastosowania w informatyce.

Centralnym problemem tej ostatniej jest pytanie, o to czy dana logika może wyrazić dane zapytanie (własność modeli nad daną sygnaturą) tzn. czy można napisać odpowiednią formułę logiczną spełnialną przez dokładnie te modele, które mają rozpatrywaną własność. Tego rodzaju dociekania teoretyczne są blisko związane z pytaniem o to czy dany język zapytań bazodanowych np. SQL jest w stanie wyrazić pewne zapytania. Rozpatruje się logiki takie, jak logika pierwszego rzędu, logika drugiego rzędu, logiki punktu stałego itd., itp. Badane zapytania odpowiadają ważnym problemom obliczeniowym takim, jak spójność grafu, spełnialność formuł Boolowskich, kolorowaniu grafów itd. itp. Aby dowieść, że logika L wyraża zapytanie Q wystarczy podać odpowiednią formułę logiczną. Dużo trudniej jest osiągnąć wynik negatywny. Pierwsza część wykładu obejmuje twierdzenia Ehrenfeuchta-Fraissego, Hanfa, Gaifmana oraz inne rezultaty, które oferują metody pozwalające na pokazywanie, że logika pierwszego rzędu nie wyraża pewnych zapytań.

Druga część kursu dotyczy złożoności obliczeniowej problemu model checkingu tj. dla danej formuły F w logice L oraz struktury S należy sprawdzić algorytmicznie, czy S jest modelem F. Omówiona zostaje szczegółowa klasyczna oraz parametryczna złożoność obliczeniowa przypadku, gdy obie F oraz S są na wejściu problemu (combined complexity), wersji gdy struktura jest parametrem (expression complexity) oraz wersja, w której formuła jest parametrem (data complexity). Omawia się również złożoność tzw. zapytań konjunktywnych (conjunctive queries), również acyklicznych zapytań konjunktywnych.

Trzecia część kursu dotyczy deskryptywnej teorii złożoność, która porównuje klasy problemów (zapytań) ze względu na siłę wyrażąnia najsłabszej logiki, która potrafi wyrazić je wszystkie. Pokazujemy znane zależności pomiędzy klasycznymi klasami złożoności i odpowiednimi logikami. Pokazujemy m.in. cały wachlarz klas obliczeń równoległych równoważnych logice pierwszego rzędu (z dodawaniem oraz mnożeniem), twierdzenie Fagina (egzystencjalna logika drugiego rzędu jest równoważna klasie NP) oraz twierdzenie Immermana-Verdiego (logika najmniejszego punktu stałego jest równa P na strukturach z porządkiem).

Literatura:

Leonid Libkin "Elements of Finite Model Theory"

Neil Immerman "Descriptive Complexity"

Heinz-Dieter Ebbinghaus , Jörg Flum "Finite Model Theory"

Opisy przedmiotów w USOS i USOSweb są chronione prawem autorskim.
Właścicielem praw autorskich jest Uniwersytet Jagielloński w Krakowie.