Výroková a predikátová logika
Cvičení probíhají ve středu v 10:40 v S6.
Požadavky na zápočet
Zápočet bude udělen za získání 140 bodů za semestr. Body lze získat třemi způsoby:
- domácí úkoly - budou zadány celkem dva úkoly po 5 bodech
- projekt na SAT solver - 35 bodů
- testy - budeme psát dva testy, za každý bude možné získat 100 bodů, zároveň potřebujete z každého získat alespoň 40 bodů (každý test můžete jednou opakovat)
- aktivita - můžete získat až 5 bodů za aktivitu - pokud budete aktivní na dvou různých cvičeních, dostanete 1 bod
Co to znamená býti aktivní? Hlavním cílem je vás motivovat k tomu, abyste se ptali nebo odpovídali na mé otázky, aktivita je tedy definována celkem široce, např. vyřešení příkladu, odpověď na otázku (nezávisle na správnosti, pokud se snažíte správně odpovědět), nebo i položení otázky týkající se probírané látky.
Domácí úkoly
- Výroková logika - termín 18. listopadu 2025 v 9:00, detaily v pdf
Další zdroje
Příklady ze cvičení
Na cvičení budeme používat především příklady z webů cvičení Petra Gregora a Jakuba Bulína. Odkazy na příklady níže se týkají právě jich, pro cvičení Petra Gregora používám zkratku PG, pro Jakuba Bulína JB.
| Datum | Téma |
|---|---|
| 1. 10. 2025 | Úvod, syntaxe vs sémantika výrokové a predikátové logiky, výrokové formule, vyjadřování formulemi (příklady 1. cv. JB - 1) |
| 8. 10. 2025 | Modely, univerzálnost spojek, převody do CNF a DNF (příklady 2. cv. JB - 1, 2, 3) |
| 15. 10. 2025 | Sémantika vzhledem k teorii, počítání počtu výroků až na ekvivalenci (příklady 2. cv JB - 4; 3. cv. JB - 1) |
| 22. 10. 2025 | SAT, 2-CNF, ukázka použití SAT solveru (příklady 3. cv. JB - 1ef, 2; PG 2. cv. - 12) |
| 29. 10. 2025 | HornSAT, DPLL, tablo metoda ve výrokové logice (příklady 4. cv. JB - 1,3,6,7,8) |
| 5. 11. 2025 | Věta o kompaktnosti, rezoluce ve výrokové logice (příklady 4. cv. JB - 2, 4; 5. cv. JB - 1, 2, 3) |