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

• termín zápočtového testu z výrokové logiky: 21. 11. Vzorový test: výroková logika
• termín zápočtového testu z predikátové logiky: 9. 1. Vzorový test: predikátová logika
• předběžný termín opravných testů (VL i PL): v prvním týdnu zkouškového období (upřesníme dle počtu nezapočtených studentů)

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.)

• Program: 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.
• Materiály: priklady3.pdf, reseni3.pdf, ukázka SAT solveru včetně řešiče Glucose, viz také ukázka použití SAT solveru na řešení Sliding Puzzle

4. cvičení (24. 10.)

• Program: Tablo metoda ve výrokové logice. Věta o kompaktnosti a její aplikace.
• Materiály: priklady4.pdf, reseni4.pdf

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.)

• Program: Rezoluce ve výrokové logice.
• Materiály: priklady5.pdf, reseni5.pdf

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, reseni7.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, reseni8.pdf

11. cvičení (12. 12.)

• Program: Převod do PNF. Skolemizace. Herbrandova věta. Unifikace.
• Materiály: priklady9.pdf, reseni9.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, reseni10.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

• Přednáška a stará přednáška doc. Gregora
• Cvičení doc. Gregora, dr. Vomlelové, a dr. Hrice

Č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.