NAIL062 Výroková a predikátová logika: cvičení (Podzim 2024)
Zde najdete informace k mým cvičením
Konzultační hodiny:
- Pondělí 15:30 (po přednášce) před N1
- Čtvrtek 14:00 v S303
nebo individuálně po předchozí domluvě (napište mi email), budou k dispozici další dvě hodiny týdně.
Zápočet
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ů. Pro každý z testů budete mít nárok na jeden opravný pokus. Žádné další opravné možnosti nebudou. Kromě testů lze získat až 50 bodů za domácí úkoly:
- 40 bodů za projekt na aplikaci SAT solveru
- 5 bodů za domácí úkol z výrokové logiky
- 5 bodů za domácí úkol z predikátové logiky
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í.
K získání zápočtu je třeba získat celkem alespoň 140 bodů, a zároveň alespoň 40 bodů z každého z testů.
Zápočtové testy
Domácí úkoly:
- Domácí úkol z výrokové logiky: termín odevzdání 14. 11. do začátku cvičení, zadání: vyřešte Vzorový test z výrokové logiky (Odevzdejte na papíře nebo emailem v jediném PDF souboru s bílým pozadím.)
- Domácí úkol z predikátové logiky: termín odevzdání 19. 12. do začátku cvičení, zadání: vyřešte Vzorový test z predikátové logiky (Odevzdejte na papíře nebo emailem v jediném PDF souboru s bílým pozadím. Část (c) prvního příkladu nebude hodnocena, nejspíše ještě nestihneme dostatečně procvičit. Doporučuji ale zkusit si vyřešit.)
- Domácí úkol na aplikaci SAT solveru: podrobné zadání, do 20. 10. zašlete své preference a problémy, do konce listopadu odevzdejte hotový projekt
Program cvičení (bude aktualizováno)
1. cvičení (3. 10.)
- Program: Úvod do výrokové logiky. Základy syntaxe a sémantiky výrokové logiky. Ukázka tablo metody a rezoluční metody.
- Materiály: priklady1.pdf, reseni1.pdf
2. cvičení (10. 10.)
- Program: Syntaxe a sémantika výrokové logiky. Univerzálnost logických spojek. Převod do CNF a DNF. Vlastnosti a extenze teorií.
- Materiály: priklady2.pdf, reseni2.pdf
3. cvičení (17. 10.)
4. cvičení (24. 10.)
5. cvičení (31. 10.)
- Program: (pokračujeme v programu předchozího cvičení, řešíme nedodělané příklady)
- Materiály: (pokračujeme v priklady4.pdf)
6. cvičení (7. 11.)
7. cvičení (14. 11.)
- Termín odevzdání Domácího úkolu z výrokové logiky
- Program: Úvod do predikátové logiky. Syntaxe a sémantika predikátové logiky.
- Materiály: priklady6.pdf, reseni6.pdf
8. cvičení (21. 11.)
- Zápočtový test z výrokové logiky
- Program: (pokračujeme v programu předchozího cvičení, řešíme nedodělané příklady)
- Materiály: (pokračujeme v priklady6.pdf)
9. cvičení (28. 11.)
- blíží termín odevzdání projektu na SAT solver
- Program: Struktury a podstruktury. Extenze teorií. Extenze o definice. Definovatelné množiny.
- Materiály: priklady7.pdf
10. cvičení (5. 12.)
- Program: Tablo metoda v predikátové logice, jazyky s rovností. Aplikace Věty o kompaktnosti.
- Materiály: priklady8.pdf
11. cvičení (12. 12.)
- Program: Převod do PNF. Skolemizace. Herbrandova věta. Unifikace.
- Materiály: priklady9.pdf
12. cvičení (19. 12.)
- Termín odevzdání Domácího úkolu z predikátové logiky
- Program: Rezoluce v predikátové logice.
- Materiály: priklady10.pdf
13. cvičení (9. 1.)
- Zápočtový test z predikátové logiky
- Program: Vybraná témata z teorie modelů.
- Materiály: (pokračujeme v priklady10.pdf)
Užitečné odkazy
Často kladené dotazy
- Co mám dělat, pokud mám otázku ke cvičení? – Podívejte se sem do ČKD. Pokud nenajdete odpověď, napište mi email; do předmětu zprávy, prosím, napište “nail062” a “cvičení”.
- Co mám dělat, pokud chci konzultaci? – Domluvte se se mnou po cvičení, přijďte na rozvržené konzultační hodiny, nebo si domluvme termín konzultace emailem.