Výroková a predikátová logika - cvičení

Rozvrh: Pátek 12:20-13:50, posluchárna S7.
Vyučující: Petr Gregor (gregor(at)ktiml.mff.cuni.cz)
Informace o přednášce: 2/2 Zk/Z NAIL062 v SISu, na stránce k přednášce

Procvičované příklady
Zde budou postupně zveřejňovány, z loňských cvičení jsou zde.

• Cvičení 1 - 05. 10.: Vyjadřování formulemi různých řádů.
• Cvičení 2 - 12. 10.: Univerzálnost spojek, reprezentovatelnost, DNF a CNF.
• Cvičení 3 - 19. 10.: 2-SAT a Horn-SAT, sémantika vzhledem k teoriím.
• Cvičení 4 - 26. 10.: Analýza teorií s konečně prvovýroky, tablo metoda.
• Cvičení 5 - 02. 11.: Rezoluce ve výrokové logice.
• Cvičení 6 - 09. 11.: Test 1, Hilbertův kalkul.
• Cvičení 7 - 16. 11.: Základní syntax a sémantika PL.
• Cvičení 8 - 23. 11.: Podstruktury, extenze, kompletnost.
• Cvičení 9 - 30. 11.: Extenze, definovatelnost.
• Cvičení 10 - 7. 12.: Tablo metoda v PL.
• Cvičení 11 - 14. 12.: Prenexní tvar, extenze o definice, skolemizace.
• Cvičení 12 - 21. 12.: Herbrandova věta, rezoluce v PL.
• Cvičení 13 - 04. 01.: Test 2, rezoluce.
• Cvičení 14 - 11. 01.: Dokončení příkladů z minula, zkouškové testy.

Hodnocení
Bude založené na bodech získaných za dva testy psané v průběhu semestru, za domácí úkoly a aktivitu na cvičeních.