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

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

Konzultační hodiny:

• Pondělí 18:50 (po přednášce) v N1
• Čtvrtek 14:00 před 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 dodatečných až 50 bodů:

• 40 bodů za projekt na aplikaci SAT solveru
• 10 bodů za aktivitu na cvičeních

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: 12. 11. Vzorový test: výroková logika
• termín zápočtového testu z predikátové logiky: 7. 1. Vzorový test: predikátová logika

Termíny opravných testů:

• opravný test z VL: první týden zkouškového období (bude upřesněno)
• opravný test z PL: první týden zkouškového období (bude upřesněno)

Projekt: aplikace SAT solveru

Podrobně si přečtěte následující zadání projektu. Dodržujte všechny pokyny v něm obsažené. Preference zadávejte v popsaném formátu, jinak na ně nebude brán zřetel. Vypracovaný projekt musí splňovat popsané požadavky.

Termíny:

• do 25. 10. zadejte vyjádření preferencí (v SISu v modulu Studijní mezivýsledky) případně zaslání vlastních návrhů problémů (emailem)
• projekt vám bude přidělen nedlouho poté, také v modulu Studijní mezivýsledky
• do 15. 11. zadejte odkaz na repozitář svého projektu (v modulu Studijní mezivýsledky)
• do konce listopadu musí repozitář obsahovat dokončený projekt (z historie commitů musí být jasně patrný průběh vývoje); k pozdějším změnám již nebude přihlíženo
• v první polovině prosince buďte připraveni předvést svůj projekt cvičícímu, budete-li k tomu vyzváni

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í

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

• Program: Pokračujeme v programu z předchozího cvičení.
• Materiály: Pokračujeme v priklady1.pdf, reseni1.pdf

3. cvičení (15. 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

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

• blíží se termín zadání preferencí příp. zaslání vlastních návrhů na SAT projekt
• 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

5. cvičení (29. 10.)

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

6. cvičení (5. 11.)

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

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

• blíží se termín zadání adresy repozitáře SAT projektu
• Zápočtový test 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í (19. 11.)

• blíží se termín odevzdání projektu na SAT solver
• Program: Syntaxe a sémantika predikátové logiky: pokračování
• Materiály: (pokračujeme v priklady6.pdf)

9. cvičení (26. 11.)

• blíží se 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í (3. 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í (10. 12.)

• Program: Převod do PNF. Skolemizace. Herbrandova věta. Unifikace. Ukázka rezoluční metody.
• Materiály: priklady9.pdf, reseni9.pdf

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

• Program: Rezoluce v predikátové logice.
• Materiály: priklady10.pdf, reseni10.pdf

13. cvičení (7. 1.)

• Zápočtový test z predikátové logiky
• Program: Vybraná pokročilejší témata.
• 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.