Tradycyjnie, logika zajmowała się prawami myślenia. Współcześnie, informatyka stwarza możliwości przetwarzania informacji na wielką skalę również poza umysłem człowieka. Nic więc dziwnego, że rozwój informatyki stawia przed logiką nowe wyzwania i fascynujące problemy. Spośród wielu możliwości, wybraliśmy następujące zagadnienia.

Teoria złożoności klasyfikuje problemy obliczeniowe ze względu na zasoby potrzebne do ich realizacji, takie jak czas i pamieć przy klasycznych obliczeniach sekwencyjnych, ale także liczba procesorów przy obliczeniach równoległych lub liczba bitów losowych w obliczeniach zrandomizowanych. Złożoność obliczeniowa jest przesłanką bezpieczeństwa w kryptografii asymetrycznej, pomimo że wiekszość jej hipotez pozostaje nieudowodniona, stanowiąc wyzwanie dla matematyki. Pomostem pomiędzy teorią złożoności a logiką jest tzw. teoria złożoności opisowej: pytania o zależności między różnymi klasami złożoności (jak np. P, NP, PSPACE) sprowadzają się w niej do pytań o równoważnosć różnych logik, przeważnie rozszerzeń logiki pierwszego rzędu o różnego rodzaju operatory punktu stałego.

Formalna weryfikacja programów. W wielu zastosowaniach od niezawodności działania oprogramowania, a także sprzętu (np. mikroprocesorów) zależą znaczne wartości ekonomiczne, a czasem nawet życie ludzi. W krytycznych zastosowaniach nie można polegać na serii testów -- poszukuje się pewniejszych metod. Jedną z nich jest budowanie matematycznego modelu wszystkich możliwych stanów systemu i sprawdzanie własności tego modelu metodami automatycznymi. Zadaniem logiki jest tu precyzyjne wyrażenie własności poprawności. Użytecznym modelem zachowania systemu jest gra o potencjalnie nieskończonym czasie trwania, w której gracz ,,system'' gra z graczem ,,środowisko''. Matematyczna weryfikacja używa szerokiej gamy metod, od logiki temporalnej i logik stałopunktowych, po elementy teorii automatów, a także teorii gier.

Klasyczna teoria automatów. Mimo, że teoria automatów rozwija się od początku istnienia informatyki, niektóre klasyczne problemy do tej pory pozostają nierozwiązane, a wciąż pojawiają się nowe. Weźmy dla przykładu wyrażenia regularne: czy istnieje język regularny, którego nie można opisać wyrażeniem regularnym bez zagnieżdżonej gwiazdki (ale z dopełnieniem)? Jest to do dziś pytanie otwarte. Na seminarium będziemy badać podobne pytania dotyczące języków regularnych skończonych słów, a także modele bardziej ogólne, jak automaty na skończonych lub nieskończonych drzewach.