NAIL062 Výroková a predikátová logika: cvičení (Podzim 2025)

Zde najdete informace k mému českému cvičení.

Konzultační hodiny:

• Pondělí 10:40 v S303
• 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

TBA

Domácí úkoly:

TBA

Příklady na cvičení

1. Úvod do výrokové logiky	priklady1.pdf	reseni1.pdf
2. Sémantika, vlastnosti teorií	priklady2.pdf	reseni2.pdf
3. Algebra výroků, Problém SAT	priklady3.pdf	reseni3.pdf
4. Tablo metoda	priklady4.pdf	reseni4.pdf
5. Rezoluční metoda	priklady5.pdf	reseni5.pdf
6. Základy predikátové logiky	priklady6.pdf	reseni6.pdf
7. Vlastnosti struktur a teorií	priklady7.pdf	reseni7.pdf
8. Tablo metoda v predikátové logice	priklady8.pdf	reseni8.pdf
9. Příprava na rezoluci v PL	priklady9.pdf	reseni9.pdf
10. Rezoluční metoda v PL	priklady10.pdf	reseni10.pdf

Program cvičení (bude aktualizováno)

1. cvičení (29. 9.)

• 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í (6. 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í (13. 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í (20. 10.)

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

5. cvičení (27. 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í (3. 11.)

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

7. cvičení (10. 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í (24. 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í (1. 12.)

• 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í (8. 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í (15. 12.)

• Termín odevzdání Domácího úkolu z predikátové logiky
• Program: Převod do PNF. Skolemizace. Herbrandova věta. Unifikace. Rezoluce v predikátové logice.
• Materiály: priklady9.pdf, reseni9.pdf, priklady10.pdf, reseni10.pdf

12. cvičení (5. 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.