Prace Churcha, Turing i Goedla z początkow XX w. pokazały, że problem
spełnialności (czy dana formuła ma model?) dla logiki pierwszego rzędu jest
nierozstrzygalny. Wyniki te zapoczątkowały duży program badawczy, ktorego
celem było ustalenie, ktore naturalne fragmenty logiki pierwszego rzędu są
rozstrzygalne. Nieco poźniej dodatkowym bodźcem dla tego programu stały się
potencjalne zastosowania w informatyce (bazy danych i reprezentacja wiedzy,
automatyczna weryfikacja programow i sprzętu, sztuczna inteligencja, itd.).
Oczywiście, zwiększyły one też zainteresowanie badaczy dokładną złożonością
obliczeniową problemu spełnialności w przypadku fragmentow rozstrzygalnych.
Na wykładzie przedstawię szereg wynikow dotyczących
rozstrzygalności/nierozstrzygalności i złożoności obliczeniowej logik
motywowanych teorią informatyki.
W programie m.in.: logiki modalne i temporalne, logiki z dwiema zmiennymi,
logiki ze strażnkiami. Wykład będzie oparty głownie na pracach opublikowanych
w ciągu ostatnich kilkunastu lat, choć opowiem oczywiście rownież o kilku
klasycznych wynikach.
******Wymagania:** Logika dla informatyk ow, Języki formalne i złożoność
obliczeniowa (zalecane)