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

Konzultační hodiny:

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

Informace o zkouškách

Podrobnosti o formátu a průběhu zkoušky, včetně seznamu zkouškových otázek (aktualizované pro ZS 2023/2024):

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

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 z Kapitoly 2
Prezentace: slides1.pdf

Program: Sémantika výrokové logiky. Normální formy (CNF, DNF). Vlastnosti a důsledky teorií. Extenze teorií.
Materiály: Sekce 2.2-2.4 z Kapitoly 2
Prezentace: slides2.pdf

Program: 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.5 z Kapitoly 2, Kapitola 3
Prezentace: slides3.pdf, ukázka SAT solveru: sat-solving.zip

Program: Úvod do metody analytického tabla. Pojem tablo důkazu. Věty o korektnosti a úplnosti a jejich důsledky.
Materiály: Sekce 4.1-4.6 z Kapitoly 4
Prezentace: slides4.pdf

Program: Věta o kompaktnosti a její důsledky. Hilbertovský kalkulus. Rezoluční metoda, korektnost, úplnost. LI-rezoluce a Horn-SAT.
Materiály: Sekce 4.7-4.8 z Kapitoly 4, Kapitola 5
Prezentace: slides5.pdf

Program: Úvod do predikátové logiky. Syntaxe a sémantika predikátové logiky. Vlastnosti teorií.
Materiály: Sekce 6.1-6.5 z Kapitoly 6
Prezentace: slides6.pdf

Program: Podstruktury, expanze a redukty. Extenze teorií, extenze o definice. Definovatelnost a databázové dotazy. Vztah výrokové a predikátové logiky.
Materiály: Sekce 6.6-6.9 z Kapitoly 6
Prezentace: slides7.pdf

Program: Tablo metoda v predikátové logice, jazyky s rovností. Korektnost a úplnost, kanonický model.
Materiály: Sekce 7.1-7.4 z Kapitoly 7
Prezentace: slides8.pdf

Program: Löwenheim-Skolemova věta, věta o kompaktnosti. Hilbertovský kalkulus. Úvod do rezoluce v predikátové logice, skolemizace
Materiály: Sekce 7.5-7.6 z Kapitoly 7, Sekce 8.1-8.2 z Kapitoly 8
Prezentace: slides9.pdf

Program: Grounding, Herbrandova věta. Unifikace, unifikační algoritmus. Rezoluční pravidlo, rezoluční důkaz.
Materiály: Sekce 8.3-8.5 z Kapitoly 8
Prezentace: slides10.pdf

Program: Korektnost rezoluce. Lifting lemma a úplnost rezoluce. LI-rezoluce a Prolog. Elementární ekvivalence.
Materiály: Sekce 8.6-8.7 z Kapitoly 8, Sekce 9.1 z Kapitoly 9
Prezentace: slides11.pdf

Program: Izomorfismus a konečné modely. Definovatelnost a automorfismy. Omega-kategoricita a úplnost. Axiomatizovatelnost. Rekurzivní axiomatizace a rozhodnutelnost.
Materiály: Sekce 9.2-9.4 z Kapitoly 9, Sekce 10.1 z Kapitoly 10
Prezentace: slides12.pdf

Program: * 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: Sekce 10.2-10.4 z Kapitoly 10
Prezentace: slides13.pdf

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.

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.