Prace Churcha, Turing i Goedla z początków 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, którego celem było ustalenie, które naturalne fragmenty logiki pierwszego rzędu są rozstrzygalne. Nieco później dodatkowym bodźcem dla tego programu stały się potencjalne zastosowania w informatyce (bazy danych, reprezentacja wiedzy,
automatyczna weryfikacja programów 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 fragmentów rozstrzygalnych.
Na wykładzie przedstawię szereg wyników dotyczących rozstrzygalności/nierozstrzygalności i złożoności obliczeniowej logik motywowanych teorią informatyki.
W programie m.in.: logiki modalne, temporalne i deskrypcyjne, logiki z dwiema zmiennymi, fragmenty strzeżone, logika z unarną negacją. Wykład będzie oparty głównie na pracach opublikowanych w
ciągu ostatnich dwudziestu kilku lat, choć opowiem oczywiście również o paru klasycznych wynikach, sięgając m.in. do prac Kurta Gödla.
**Wymagania:** Logika dla informatyków, Zalecane: Języki formalne i złożoność obliczeniowa
**W razie konieczności prowadzenia zajęć zdalnie**: wykłady
i ćwiczenia będą odbywały się online przy użyciu wybranej
platformy (np. MS Teams).
