Teoria modeli skończonych 1000-2M13TSK

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.