Přednáška: Čtvrtek, 17:20, S10 (Jakub Bulín)
Cvičení: Čtvrtek, 9:00, S6 (Martin Blicha)
Stránka v SIS: NAIL062
Zakončení: Zkouška a zápočet
Zápočet
K získání zápočtu je třeba získat celkem 120 bodů.
V průběhu semestru budou dva zápočtové testy (na 45 minut). První (zhruba v polovině semestru) bude pokrývat část přednášky “Výroková logika”, druhý (ke konci semestru) část přednášky “Predikátová logika”. Za každý z testů lze získat maximálně 100 bodů. Kromě toho lze získat maximálně 20 bodů za domácí úkoly.
Na konci semestru bude možnost opravit si výsledek horšího z těchto dvou testů napsáním opravného testu (termín bude v prvních dvou týdnech zkouškového období). Žádné další opravné možnosti nebudou.
Pokud student zamešká některý z testů ze zdravotních důvodů, může si tento také nahradit napsáním opravného testu. V případě onemocnění v termínu opravného testu bude zorganizován náhradní termín.
Domácí úkoly
V průběhu semestru budou zadány dva domácí úkoly, které vám pomůžou připravit se na zápočtové testy.
Za každý úkol můžete získat maximálně 10 bodů.
Užitečné odkazy
Program cvičení (bude průběžně aktualizován)
1. cvičení (5.10.)
- Program: Úvod. Formalizace tvrzení ve výrokové a predikátové logice.
- Materiály: příklady, přehled matematických pojmů
2. cvičení (12.10.)
- Program: Formalizace ve výrokové logice. Syntaxe a sémantika výrokové logiky.
- Materiály: příklady
3. cvičení (19.10.)
- Program: Teorie ve výrokové logice. Převod do CNF a DNF. Univerzálnost logických spojek.
- Materiály: příklady
4. cvičení (26.10.)
- Program: Vlastnosti a extenze teorií. Počítání výroků až na ekvivalenci. 2-SAT a implikační graf. Horn-SAT a jednotková propagace. Ukázka SAT solveru.
- Materiály: příklady
5. cvičení (2.11.)
- Děkanský sportovní den, cvičení odpadá!
6. cvičení (9.11.)
-
První domácí úkol: zadání. Termín odevzdání 23.11.
-
Program: Tablo metoda ve výrokové logice.
-
Materiály: příklady, SAT/SMT by Example
7. cvičení (16.11.)
- Program: Rezoluce ve výrokové logice. Hilbertův kalkulus.
- Materiály: příklady
8. cvičení (23.11.)
- Program: Syntaxe a sémantika predikátové logiky.
- Materiály: příklady
9. cvičení (30.11.)
- 1. zápočtový test
- Program: Dokončení sémantiky predikátové logiky. Struktury.
- Materiály: příklady z 8. cvičení
10. cvičení (7.12.)
- Druhý domácí úkol:. Termín odevzdání 21.12.
- Program: Struktury a podstruktury. Extenze teorií. Extenze o definice. Definovatelné množiny. Tablo metoda v predikátové logice, jazyky s rovností.
- Materiály:
11. cvičení (14.12.)
- Program: Aplikace Věty o kompaktnosti. Ještě tablo metoda. Převod do PNF. Skolemizace. Herbrandova věta.
- Materiály:
12. cvičení (21.12.)
- Program: Rezoluce v predikátové logice.
- Materiály:
13. cvičení (4.1.)
- 2. zápočtový test
- Program: Vybraná témata z teorie modelů.
- Materiály:
14. cvičení (11.1.)
- Program: Ukázka použití řešičů pro verifikaci software
- Materiály: