viz anglická verze
V přednášce se studenti seznámí se základními pojmy z teorie důkazů (důkazovými systémy pro výrokovou a predikátovou logiku) a základními výsledky této teorie (Herbrandova věta, věta o eliminaci řezů, Craigova věta o interpolaci). Tyto výsledky budou studovány z hlediska složitosti; ukážeme i některé dolní odhady na složitost důkazů.
Dále se přednáška zabývá také přepisováním termů (v případě dostatku času, lambda kalkulem) a připomeneme si i Godelovy věty o neúplnosti.