Základní kocepty teorie výpočetní složitosti. Definovatelnost v logice prvního řádu.
Konečná teorie modelů. Důkazová složitost a SAT algoritmy, Herbrandova věta a dosvědčující věty.
Přednáška probírá souvislosti mezi matematickou logikou a teorií výpočetní složitosti.
Předmět nemusí být vyučován každý rok.