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

Zde najdete informace k mému cvičení (Pondělí 10:40 v S7, nebo možná v S4?).

Konzultační hodiny:

• Pondělí 12:20 v S303
• Čtvrtek 18:50 v N1

nebo individuálně po předchozí domluvě emailem.

Program cvičení (bude aktualizováno)

1. cvičení (2. 10.)

• Program: Úvod. Vyjadřování různých vlastností ve výrokové a predikátové logice. Připomenutí matematických pojmů.
• Materiály: cviceni1.pdf, případně také přehled matematických pojmů

2. cvičení (9. 10.)

• Program: Formalizace ve výrokové logice. Syntaxe a sémantika výrokové logiky. Ukázka tablo metody a rezoluční metody.
• Materiály: cviceni2.pdf

3. cvičení (16. 10.)

• Program: Syntaxe a sémantika výrokové logiky. Převod do CNF a DNF. Univerzálnost logických spojek.
• Materiály: cviceni3.pdf

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

• Program: Vlastnosti a extenze teorií. Počítání výroků až na ekvivalenci. 2-SAT a implikační graf. Horn-SAT a jednotková propagace.
• Materiály: cviceni4.pdf, ukázka SAT solveru včetně řešiče Glucose

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

• Program: Algoritmus DPLL. Kódování problémů do SAT. Tablo metoda ve výrokové logice.
• Materiály: cviceni5.pdf

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

• Program: Ještě tablo metoda: aplikace a pokročilejší problémy. Ukázka rezoluční metody.
• První domácí úkol: du1.pdf. Termín odevzdání: 20. 11. v 10:40
• Materiály: cviceni6.pdf

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

• Program: Rezoluce ve výrokové logice. Aplikace věty o kompaktnosti. Hilbertův kalkulus.
• Materiály: cviceni7.pdf

8. cvičení (20. 11.)

• Program: Syntaxe a sémantika predikátové logiky.
• Materiály: cviceni8.pdf
• nezapomeňte odevzdat první domácí úkol

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

• 1. zápočtový test
• Program: Struktury a podstruktury. Extenze teorií.
• Materiály: cviceni9.pdf

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

• Program: Extenze o definice. Definovatelné množiny. Tablo metoda v predikátové logice, jazyky s rovností.
• Druhý domácí úkol: du2.pdf. Termín odevzdání: 18. 12. v 10:40
• Materiály: cviceni10.pdf

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

• Program: Aplikace Věty o kompaktnosti. Ještě tablo metoda. Převod do PNF. Skolemizace. Herbrandova věta.
• Materiály: cviceni11.pdf

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

• Program: Rezoluce v predikátové logice.
• Materiály: cviceni12.pdf
• nezapomeňte odevzdat druhý domácí úkol

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

• 2. zápočtový test
• Program: Vybraná témata z teorie modelů.
• Materiály: cviceni13.pdf

Užitečné odkazy

• Přednáška a stará přednáška doc. Gregora

• Cvičení doc. Gregora, dr. Vomlelové, a dr. Hrice

Zápočet

• Podmínky pro získání zápočtu
• předběžný termín 1. zápočtového testu (výroková logika): 27. 11. Vzorový test: výroková logika
• předběžný termín 2. zápočtového testu (predikátová logika): 8. 1. Vzorový test: predikátová logika
• předběžný termín opravného testu: v prvních dvou týdnech zkouškového období

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