NAIL062 Výroková a predikátová logika
- 🇬🇧 The English lecture of NAIL062 by Petr Gregor is under this link.
- 🇨🇿 Zde najdete informace o české přednášce Jakuba Bulína.
Podrobnosti o formátu a průběhu zkoušky, včetně seznamu zkouškových otázek, najdete v tomto PDF:
Program přednášek
Zápisky z přednášky, pro tento semestr už neočekávám zásadní změny, jen opravy chyb:
První přednáška (3. 10.)
- Program: Úvod do logiky, neformální představení výrokové a predikátové logiky. Syntaxe výrokové logiky.
- Materiály: Kapitola 1; Sekce 2.1.1-2.1.2 z Kapitoly 2
Druhá přednáška (10. 10.)
- Program: Syntaxe a sémantika výrokové logiky. Normální formy (CNF, DNF). Vlastnosti a důsledky teorií.
- Materiály: Sekce 2.1.3-2.4.1 z Kapitoly 2
Třetí přednáška (17. 10.)
- Program: Extenze teorií. Algebra výroků. Problém splnitelnosti, SAT solvery. 2-SAT a implikační graf. Horn-SAT a jednotková propagace. Algoritmus DPLL
- Materiály: Sekce 2.4.2 a 2.5 z Kapitoly 2; Kapitola 3
Čtvrtá přednáška (24. 10.)
- Program: Úvod do metody analytického tabla. Pojem tablo důkazu. Věta o korektnosti a úplnosti a jejich důsledky.
- Materiály: Sekce 4.1-4.6
Pátá přednáška (31. 10.)
- Program: Věta o kompaktnosti a její důsledky. Hilbertovský kalkulus. Rezoluční metoda, korektnost, úplnost.
- Materiály: Sekce 4.7-4.8, 5.1-5.3
Šestá přednáška (7. 11.)
- Program: LI-rezoluce, rezoluce v Prologu. Úvod do predikátové logiky. Syntaxe predikátové logiky.
- Materiály: Sekce 5.4-5.5, 6.1-6.3
Sedmá přednáška (14. 11.)
- Program: Sémantika predikátové logiky. Vlastnosti teorií. Podstruktury, expanze a redukty. Věta o konstantách.
- Materiály: Sekce 6.4-6.6
Osmá přednáška (21. 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-7.3
Devátá přednáška (28. 11.)
- Program: Korektnost tablo metody, kanonický model, úplnost. Löwenheim-Skolemova věta, věta o kompaktnosti. Hilbertovský kalkulus. Úvod do rezoluce v predikátové logice.
- Materiály: Sekce 7.4-8.1
Desátá přednáška (5. 12.)
- Program: Ekvisplnitelnost, převod do PNF, Skolemizace. Grounding, Herbrandův model, Herbrandova věta. Skládání substitucí.
- Materiály: Sekce 8.2-8.4.1
Jedenáctá přednáška (12. 12.)
- Program: Unifikační algoritmus. Rezoluční pravidlo, rezoluční důkaz. Korektnost rezoluce. Lifting lemma a úplnost rezoluce. LI-rezoluce, Prolog.
- Materiály: Sekce 8.4.2-8.7
Dvanáctá přednáška (19. 12.)
- Program: Elementární ekvivalence. Důsledky Löwenheim-Skolemovy věty. Izomorfismus a konečné modely. Definovatelnost a automorfismy. Omega-kategoricita a úplnost.
- Materiály: Kapitola 9
Třináctá přednáška (2. 1.)
- Program: * Rozhodnutelnost. Rekurzivní axiomatizovatelnost. Rozhodnutelné teorie: příklady. Aritmetické teorie (Robinson, Peano), Hilbertův 10. problém. Nerozhodnutelnost predikátové logiky. Gödelovy věty o neúplnosti.
- Materiály: Kapitola 10
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ění).
- 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.