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

Rozvrh: Úterý 17:20-18:50, posluchárna S11.
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

• Cvičení 1 - 08. 10. 2013: Vyjadřování formulemi různých řádů.
• Cvičení 2 - 15. 10. 2013: Dokončení předchozích příkladů, univerzálnost spojek, DNF a CNF.
• Cvičení 3 - 22. 10. 2013: Dokončení z minula, sémantika v teorii, důsledek.
• Cvičení 4 - 29. 10. 2013: Analýza teorii s konečně prvovýroky, tablo metoda ve VL.
• Cvičení 5 - 05. 11. 2013: Tablo metoda (pokr.), kompaktnost, rezoluční metoda ve VL.
• Cvičení 6 - 12. 11. 2013: 1. test, rezoluční metoda ve VL (pokr.), Hilbertovský kalkul.
• Cvičení 7 - 19. 11. 2013: Základní syntax a sémantika PL.
• Cvičení 8 - 26. 11. 2013: Modely teorií, extenze, podstruktury.
• Cvičení 9 - 03. 12. 2013: Tablo metoda v PL.
• Cvičení 10 - 10. 12. 2013: Tablo metoda v PL (pokr.), kompaktnost, skolemizace.
• Cvičení 11 - 17. 12. 2013: 2. test, extenze o definice, Herbrandovy modely, rezoluce v PL.
• Cvičení 12 - 7. 1. 2014: Kompletnost, definovatelnost, axiomatizovatelnost, aritmetiky.

Hodnocení
Bude založené na bodech získaných za tři testy psané v průběhu semestru. Pro zápočet je třeba získat alespoň 11 bodů celkem ze dvou nejlépe ohodnocených testů. Bonusové body bude možné získat za aktivitu na cvičeních.