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

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

Konzultační hodiny:

• Pondělí 15:30 (po přednášce) v N1
• Středa 15:40 v S303
• Čtvrtek 14:00 V S303

nebo individuálně po předchozí domluvě (napište mi email).

Informace o zkouškách: budou zveřejněny později

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

První přednáška (30. 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

Druhá přednáška (7. 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

Třetí přednáška (14. 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, ukázka SAT solveru: sat-solving.zip

Čtvrtá přednáška (21. 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

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

• 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

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

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

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

• Program: 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.8-6.9 z Kapitoly 6, Sekce 7.1-7.3 z Kapitoly 7
• Prezentace: slides7.pdf

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

• Program: Korektnost a úplnost tablo metody v predikátové logice, kanonický model. Věta o kompaktnosti. Hilbertovský kalkulus.
• Materiály: Sekce 7.4, 7.5.2-7.5.3, Sekce 7.6 (+ Sekce 4.8) z Kapitoly 7 (Podsekci 7.5.1 zatím přeskočíme)
• Prezentace: slides8.pdf

Devátá přednáška (2. 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

Desátá přednáška (9. 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

Jedenáctá přednáška (16. 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

Dvanáctá přednáška (6. 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
• Prezentace: slides12.pdf, slides13.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.