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

• 🇨🇿 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í 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ě.

Informace o zkouškách

Podrobnosti o formátu a průběhu zkoušky, včetně seznamu zkouškových otázek, upřesníme později. Pro netrpělivé, zde jsou informace platné pro loňský rok, nicméně očekávejte alespoň nějaké změny:

• Informace o zkouškách z loňského roku

Program přednášek (bude aktualizováno)

Zápisky z přednášky (v průběhu semestru se na nich bude ještě pracovat):

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

Prezentace ze všech přednášek (bude průběžně aktualizováno):

• Všechny prezentace

První přednáška (29. 9.)

• Program: Úvod do logiky, neformální představení výrokové a predikátové logiky. Syntaxe výrokové logiky. Sémantika výrokové logiky (začátek)
• Materiály: Kapitola 1, Sekce 2.1-2.2.4 z Kapitoly 2
• Prezentace: slides1.pdf, handout1.pdf

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

• Program: Sémantika výrokové logiky (pokračování). Normální formy (CNF, DNF). Vlastnosti a důsledky teorií. Extenze teorií. Algebra výroků.
• Materiály: Sekce 2.2.5-2.5 z Kapitoly 2
• Prezentace: slides2.pdf, handout2.pdf

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

• Program: Problém splnitelnosti, SAT solvery. 2-SAT a implikační graf. Horn-SAT a jednotková propagace. Algoritmus DPLL. Úvod do metody analytického tabla.
• Materiály: Kapitola 3, Sekce 4.1-4.2 z Kapitoly 4
• Prezentace: slides3.pdf, handout3.pdf, ukázka SAT solveru: sat-solving-example.zip (viz také ukázka použití SAT solveru na řešení Sliding Puzzle)

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

• Program: Pojem tablo důkazu. Věty o korektnosti a úplnosti a jejich důsledky. Věta o kompaktnosti a její důsledky.
• Materiály: Sekce 4.3-4.7 z Kapitoly 4 (Sekci 4.8 zatím přeskočíme)
• Prezentace: slides4.pdf, handout4.pdf

Pátá přednáška (27. 10.)

• Program: Rezoluční metoda, korektnost, úplnost. Úvod do predikátové logiky. Syntaxe predikátové logiky.
• Materiály: Sekce 5.1-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 (3. 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 (10. 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, jazyky s rovností.
• Materiály: Sekce 6.7-6.9 z Kapitoly 6, Sekce 7.1-7.3 z Kapitoly 7
• Prezentace: slides7.pdf, handout7.pdf

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

• Program: 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.4-7.6 (+ Sekce 4.8) z Kapitoly 7
• Prezentace: slides8.pdf, handout8.pdf

Devátá přednáška (1. 12.)

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

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

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

• Program: LI-rezoluce a Prolog. Elementární ekvivalence. Izomorfismus a konečné modely. Definovatelnost a automorfismy. Omega-kategoricita a úplnost.
• Materiály: Sekce 8.7 (+ Sekce 5.4) z Kapitoly 8, Sekce 9.1 (+ Podsekce 7.5.1), Sekce 9.2-9.3 z Kapitoly 9
• Prezentace: slides11.pdf, handout11.pdf

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

• Program: Axiomatizovatelnost. Rekurzivní axiomatizace a rozhodnutelnost. Nerozhodnutelnost predikátové logiky. Gödelovy věty o neúplnosti.
• Materiály: Sekce 9.4 z Kapitoly 9, 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.