Výroková a predikátová logika
Cvičení k přednášce Výroková a predikátová logika
Organizace
K získání zápočtu je třeba získat celkem alespoň 140 bodů (z 250 možných), a zároveň alespoň 40 bodů z každého z testů.
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” (vzorový test), druhý (ke konci semestru) část přednášky “Predikátová logika”(vzorový test). Za každý z testů lze získat maximálně 100 bodů. Pro každý z testů budete mít nárok na jeden opravný pokus na začátku zkouškového období. Žádné další opravné možnosti nebudou. Kromě testů lze získat až 40 bodů za projekt na aplikaci SAT solveru a 10 bodů za aktivitu na hodinách.
Účast na cvičení není povinná, nicméně je velice doporučovaná, protože se na cvičení většinou dozvíte užitečné rady, které vám usnadní řešení zápočtových písemek i projektu.
SAT projekt
Podrobné zadání projektu naleznete zde. Do 26.10. zašlete své preference na problémy, do 30.11. odevzdejte hotový projekt mailem (zip nebo odkaz na repozitář).
Je zakázáno o úkolech až do termínu odevzdání jakýmkoliv způsobem komunikovat s kýmkoliv kromě cvičícího. Řešení musí být 100% vaší vlastní prací, a je vaší povinností zajistit, že žádná další osoba nebude mít přístup k vašemu řešení.
Co bylo probráno
Zde bude krátké shrnutí každé hodiny včetně PDF se zadáním příkladů.
Pondělí 9:00 S7
29.9.
- Organizace, úvod do výrokové logiky
- priklady1.pdf, reseni1.pdf
6.10.
- Pokračování v předešlém cvičení
13.10.
- Univerzálnost logických spojek. Převod do CNF a DNF. Vlastnosti a extenze teorií.
- priklady2.pdf, reseni2.pdf
20.10.
- Počítání výroků až na ekvivalenci. 2-SAT a implikační graf. Horn-SAT a jednotková propagace. Algoritmus DPLL. Kódování problémů do SAT.
- priklady3.pdf, reseni3.pdf
27.10.
- Tablo metoda ve výrokové logice.
- priklady4.pdf, reseni4.pdf
3.11.
- Rezoluce ve výrokové logice.
- priklady5.pdf, reseni5.pdf
10.11.
- Test z VL
- Úvod do predikátové logiky. Syntaxe a sémantika predikátové logiky.
- priklady6.pdf, reseni6.pdf
17.11.
- státní svátek, odpadá!
24.11.
- Pokračování z předešlého cvičení
- Struktury a podstruktury. Extenze teorií. Extenze o definice. Definovatelné množiny.
- priklady7.pdf, reseni7.pdf
1.12.
- Tablo metoda v predikátové logice, jazyky s rovností. Aplikace Věty o kompaktnosti.
- priklady8.pdf, reseni8.pdf
8.12.
- Převod do PNF. Skolemizace. Herbrandova věta. Unifikace.
- priklady9.pdf, reseni9.pdf
15.12.
- Rezoluce v predikátové logice.
- priklady10.pdf, reseni10.pdf
5.1.
- Test z PL
Čtvrtek 10:40 S6
2.10.
- Organizace, úvod do výrokové logiky
- priklady1.pdf, reseni1.pdf
9.10.
- Univerzálnost logických spojek. Převod do CNF a DNF. Vlastnosti a extenze teorií.
- priklady2.pdf, reseni2.pdf
16.10.
- Počítání výroků až na ekvivalenci. 2-SAT a implikační graf. Horn-SAT a jednotková propagace. Algoritmus DPLL. Kódování problémů do SAT.
- priklady3.pdf, reseni3.pdf
23.10.
- Tablo metoda ve výrokové logice.
- priklady4.pdf, reseni4.pdf
30.10.
- Rezoluce ve výrokové logice.
- priklady5.pdf, reseni5.pdf
6.11.
- Test z VL
- Úvod do predikátové logiky. Syntaxe a sémantika predikátové logiky.
- priklady6.pdf, reseni6.pdf
13.11.
- Pokračování z předešlého cvičení
20.11.
- Struktury a podstruktury. Extenze teorií. Extenze o definice. Definovatelné množiny.
- priklady7.pdf, reseni7.pdf
27.11.
- Tablo metoda v predikátové logice, jazyky s rovností. Aplikace Věty o kompaktnosti.
- priklady8.pdf, reseni8.pdf
4.12.
- Převod do PNF. Skolemizace. Herbrandova věta. Unifikace.
- priklady9.pdf, reseni9.pdf
11.12.
- Rezoluce v predikátové logice.
- priklady10.pdf, reseni10.pdf
18.12.
- Podle toho, co nestihneme
8.1.
- Test z PL