Przegląd wyników dotyczących rozstrzygalności/nierozstrzygalności problemu
spełnialności (czy dana formuła ma model?) dla fragmentów logiki pierwszego
rzędu. Wykład byłby w połowie oparty na książce ,,Classical Decision Problem''
(Borger, Gradel, Gurevich), a w połowie na nowszych pracach. W programie:
klasy definiowane za pomocą prefiksu kwantyfikatorów, klasy z ograniczoną
liczbą zmiennych, logiki ze strażnkiami.
**Program:** **Wymagania:** Logika dla informatyków (zalecane) Języki formalne
i złożoność obliczeniowa