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

Rozvrh: Středa 10:40-12:10, posluchárna S6.
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 - 02. 10.: Vyjadřování formulemi různých řádů.
• Cvičení 2 - 09. 10.: Univerzálnost spojek, DNF a CNF, 2-SAT.
• Cvičení 3 - 16. 10.: Horn-SAT, sémantika vzhledem k teoriím.
• Cvičení 4 - 23. 10.: Analýza teorií s konečně prvovýroky, tablo metoda.
• Cvičení 5 - 30. 10.: Rezoluce ve výrokové logice.
• Cvičení 6 - 06. 11.: Hilbertův kalkul. Základní syntax PL.
• Cvičení 7 - 13. 11.: Test 1. Sémantika PL.
• Cvičení 8 - 20. 11.: Sémantika PL, podstruktury.
• Cvičení 9 - 27. 11.: Extenze, definovatelnost.
• Cvičení 10 - 04. 12.: Tablo metoda v PL.
• Cvičení 11 - 11. 12.: Prenexní tvar, extenze o definice, skolemizace.
• Cvičení 12 - 18. 12.: Herbrandova věta, rezoluce v PL.
• Cvičení 13 - 08. 01.: Test 2. Kategoričnost, kompletnost.

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.