Opravná písemka: PL

Max. bodů 12 : 2, 3, 1 ; 2, 4

Opraveno, body celkové i podrobné

Příklady: 1a) příprava na rezoluci, b) rezoluce, c) Herbrandovo univerzum ; 2a) Formalizace (počítačových) "virusů", b) tablo

----- časté chyby

1a) Dokazovaná formule se upraví na negaci uzávěru. Z původně volných proměnných vzniknou obecné kvantifikované, díky negaci existenčně kvantifikované a následně díky Skolemizaci konstanty.