NAIL062 Výroková a predikátová logika (Podzim 2026)

• 🇨🇿 Zde najdete informace o české přednášce Jakuba Bulína.
• 🇨🇿 Stránky mého cvičení jsou tady.
• 🇬🇧 The English lecture of NAIL062 by Petr Gregor is under this link.
• 🇬🇧 The webpage of my English tutorial class is here.

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 dodatečné dvě hodiny týdně.

Informace o zkouškách

Podrobnosti o formátu a průběhu zkoušky, včetně seznamu zkouškových otázek:

• Informace o zkouškách

Program přednášek

Zápisky z přednášky:

• Zápisky z přednášky (nově je k dispozici i anglický překlad)

Prezentace ze všech přednášek:

• Všechny prezentace

První přednáška (5. 10.)

• Program: Úvod do logiky, neformální představení logiky. Syntaxe a sémantika výrokové logiky.
• Materiály: Kapitola 1, Sekce 2.1-2.2.5 z Kapitoly 2
• Prezentace: slides1.pdf, handout1.pdf

Druhá přednáška (12. 10.)

• Program: Univerzálnost logických spojek. Normální formy (CNF, DNF). Vlastnosti a důsledky teorií. Extenze teorií. Algebra výroků. Problém splnitelnosti, SAT solvery.
• Materiály: Sekce 2.2.6-2.5 z Kapitoly 2, Sekce 3.1 z Kapitoly 3
• Prezentace: slides2.pdf, handout2.pdf, ukázka SAT solveru: sat-solving-example.zip (viz také ukázka použití SAT solveru na řešení Sliding Puzzle)

Třetí přednáška (19. 10.)

• Program: 2-SAT a implikační graf. Horn-SAT a jednotková propagace. Algoritmus DPLL. Úvod do metody analytického tabla. Pojem tablo důkazu.
• Materiály: Sekce 3.2-3.4 z Kapitoly 3, Sekce 4.1-4.3 z Kapitoly 4
• Prezentace: slides3.pdf, handout3.pdf

Čtvrtá přednáška (26. 10.)

• Program: Věty o korektnosti a úplnosti a jejich důsledky. Věta o kompaktnosti a její důsledky. Úvod do rezoluční metody, rezoluční důkaz.
• Materiály: Sekce 4.4-4.7 z Kapitoly 4 (Sekci 4.8 zatím přeskočíme), Sekce 5.1-5.2 z Kapitoly 5.
• Prezentace: slides4.pdf, handout4.pdf

Pátá přednáška (2. 11.)

• Program: Korektnost a úplnost rezoluční metody. Úvod do predikátové logiky. Syntaxe predikátové logiky.
• Materiály: Sekce 5.3 z Kapitoly 5 (Sekci 5.4 zatím přeskočíme), Sekce 6.1-6.3 z Kapitoly 6
• Prezentace: slides5.pdf, handout5.pdf

Šestá přednáška (9. 11.)

• Program: Sémantika predikátové logiky. Vlastnosti teorií. Podstruktury, expanze a redukty.
• Materiály: Sekce 6.4-6.6 z Kapitoly 6
• Prezentace: slides6.pdf, handout6.pdf

Sedmá přednáška (16. 11.)

• Program: Extenze teorií, extenze o definice. Definovatelnost a databázové dotazy. Vztah výrokové a predikátové logiky. Tablo metoda v predikátové logice.
• Materiály: Sekce 6.7-6.9 z Kapitoly 6, Sekce 7.1-7.2 z Kapitoly 7
• Prezentace: slides7.pdf, handout7.pdf

Osmá přednáška (23. 11.)

• Program: Jazyky s rovností. Korektnost a úplnost tablo metody v predikátové logice, kanonický model. Věta o kompaktnosti, Löwenheim-Skolemova věta. Hilbertovský kalkulus.
• Materiály: Sekce 7.3-7.6 z Kapitoly 7 (+ Sekce 4.8)
• Prezentace: slides8.pdf, handout8.pdf

Devátá přednáška (30. 11.)

• Program: Úvod do rezoluce v predikátové logice, Skolemizace, Grounding, Herbrandova věta.
• Materiály: Sekce 8.1-8.3 z Kapitoly 8
• Prezentace: slides9.pdf, handout9.pdf

Desátá přednáška (7. 12.)

• Program: Unifikace, unifikační algoritmus. Rezoluční pravidlo, rezoluční důkaz. Korektnost rezoluce. Lifting lemma a úplnost rezoluce. LI-rezoluce a Prolog.
• Materiály: Sekce 8.4-8.7 z Kapitoly 8 (+ Sekce 5.4)
• Prezentace: slides10.pdf, handout10.pdf

Jedenáctá přednáška (14. 12.)

• Program: Elementární ekvivalence. Izomorfismus a konečné modely. Definovatelnost a automorfismy. Omega-kategoricita a úplnost. Axiomatizovatelnost.
• Materiály: Kapitola 9
• Prezentace: slides11.pdf, handout11.pdf

Dvanáctá přednáška (4. 1.)

• Program: Rekurzivní axiomatizace a rozhodnutelnost. Nerozhodnutelnost predikátové logiky. Gödelovy věty o neúplnosti.
• Materiály: Kapitola 10, jako doplňující materiál doporučuji YouTube video z přednášky Ryana O’Donnella o Gödelových větách z cyklu Great Ideas in Theoretical Computer Science
• Prezentace: slides12.pdf, handout12.pdf

Užitečné odkazy

• Informace o předmětu v SISu. Najdete tam mj. sylabus, literaturu, a po přihlášení i záznamy přednášek doc. Gregora z minulých let.
• Přednáška doc. Gregora z minulých let. Obsah se shoduje z ~85% s naší přednáškou, najdete zde prezentace, a mnoho příkladů (z předchozích zkoušek, formát zkoušky se ale změnil).
• Moje cvičení, kde najdete příklady k procvičení. Informace o vašem cvičení vám poskytne váš cvičící.
• Přehled potřebných matematických pojmů (prezentace doc. Gregora); většinu byste už měli znát, k těm méně obvyklým se ještě vrátíme, až je budeme potřebovat.

Často kladené dotazy

• Co mám dělat, pokud mám otázku k přednášce? – Podívejte se sem do ČKD. Pokud nenajdete odpověď, napište mi email; do předmětu zprávy, prosím, napište “nail062”.

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

• Bude přednáška přenášena online nebo nahrávána? – Ne, ale v SISu najdete záznamy přednášky doc. Gregora z minulých let, které lze využít jako doplňkový studijní materiál.