Celem przedmiotu jest omówienie wybranych zagadnień związanych z pojęciem dowodu jako obiektu matematycznego, który ma precyzyjnie określoną strukturę i którego własności możemy formalnie opisywać. Elementy teorii dowodu pojawiały się już przy innych okazjach, m. in. w związku z wnioskowaniem w logice konstruktywnej i izomorfizmem Curry'ego-Howarda.
Seminarium będzie obejmowało wykłady wprowadzające, prezentacje studentów oraz część praktyczną.
Najważniejsze zagadnienia:
1. Formalne systemy wnioskowania i ich własności. Dedukcja naturalna, rachunek sekwentów, system Hilberta dla logiki intuicjonistycznej.
2. Normalizacja dowodów.
3. Systemy wnioskowania dla logiki klasycznej i logik pośrednich.
4. Translacje pomiędzy systemami logicznymi.
5. Problem automatycznego znajdowania dowodów w systemach logicznych.
