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 17:15 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. Také není povoleno při vypracování používat nástroje generativní AI. Ř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: 24. 11. Vzorový test: výroková logika
• termín zápočtového testu z predikátové logiky: 5. 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í 10. 11. do začátku cvičení, zadání: vyřešte Vzorový test z výrokové logiky (Odevzdejte na papíře nebo v SISu (v SISu v modulu Studijní mezivýsledky) v jediném PDF souboru s bílým pozadím.)
• Domácí úkol z predikátové logiky: termín odevzdání 15. 12. do začátku cvičení, zadání: vyřešte Vzorový test z predikátové logiky (Odevzdejte na papíře nebo v SISu (v SISu v modulu Studijní mezivýsledky) v jediném PDF souboru s bílým pozadím. Části (b),(c) prvního příkladu nebudou hodnoceny, 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 25. 10. zašlete své preference a problémy, do konce listopadu odevzdejte hotový projekt (v SISu v modulu Studijní mezivýsledky zadejte adresu repozitáře).

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: Pokračujeme v programu z předchozího cvičení.
• Materiály: Pokračujeme v priklady1.pdf, reseni1.pdf

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

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

• Program: Tablo metoda ve výrokové logice. Věta o kompaktnosti a její aplikace.
• Materiály: priklady4.pdf, reseni4.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
• blíží termín odevzdání projektu na SAT solver
• 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.)

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