Výroková a predikátová logika

Rozvrh: Pátek 9:00-10:30, posluchárna S3.
Přednášející: Petr Gregor (gregor(at)ktiml.mff.cuni.cz)
Informace k přednášce: 2/2 Zk/Z NAIL062 v SISu

Plán přednášky
Plán je pouze orientační, téměř jistě nebude dodržen.

Úvod
• 04.10. Přednáška 1: Trocha historie, paradoxy, jazyk matematiky, rozdíl a vztah syntaxe a sémantiky, předběžnosti, stromy, Königovo lemma.

Výroková logika
• 11.10. Přednáška 2: Základní syntax a sémantika VL, univerzálnost logických spojek, normální tvary, 2-SAT a Horn-SAT, teorie, sémantika vzhledem k teorii.
• 18.10. Přednáška 3: Důsledek teorie, vlastnosti teorií ve VL, algebra výroků. Tablo metoda pro VL.
• 25.10. Přednáška 4: Tablo metoda: systematické tablo, korektnost a úplnost. Kompaktnost.
• 01.11. Přednáška 5: Hilbertovský kalkul. Rezoluční metoda, korektnost a úplnost, lineární rezoluce, rezoluce pro Prolog.

Predikátová logika
• 08.11. Přednáška 6: Základní syntax PL, instance a varianty. Základní sémantika PL, struktury, platnost ve struktuře, v teorii, model teorie.
• 15.11. Přednáška 7: Vlastnosti teorií. Podstruktury, otevřené teorie. Expanze, redukt, věta o konstantách. Booleovy algebry. Tablo metoda pro PL.
• 22.11. Přednáška 8: Tablo metoda v PL: systematické tablo, rovnost, korektnost a úplnost.
• 29.11. Přednáška 9: Důsledky věty o úplnosti. Hilbertovský kalkul v PL. Extenze o definice. Prenexní tvar.
• 06.12. Přednáška 10: Skolemizace, Herbrandova věta. Rezoluční metoda v PL: substituce, unifikace.
• 13.12. Přednáška 11: Rezoluce v PL: rezoluční důkaz, korektnost a úplnost, lineární rezoluce a LI-rezoluce. Elementární ekvivalence, kompletnost.
• 20.12. Přednáška 12: Isomorfismus struktur, kategoričnost. Konečná a otevřená axiomatizovatelnost. Definovatelné množiny. Základní matematické teorie. Aritmetické teorie.

Nerozhodnutelnost, neúplnost
• 03.01. Přednáška 13: Rozhodnutelné teorie, rekurzivní axiomatizovatelnost. Nerozhodnutelnost PL. Věty o neúplnosti - úvod.
• 10.01. Přednáška 14: Aritmetizace syntaxe, princip self-reference, věta o pevném bodě, nedefinovatelnost pravdy. Věty o neúplnosti, důsledky. Závěr.

Doporučená literatura

• A. Nerode, R.A. Shore, Logic for Applications, Springer, 2. vydání, 1997.
• V. Švejdar, Logika, neúplnost, složitost a nutnost, Academia, Praha, 2002.
• W. Hodges, Shorter Model Theory, Cambridge University Press, 1997.


• J. Mlček, Výroková a predikátová logika, el. skripta, 2012.
• P. Štěpánek, Meze formální metody, el. skripta, 2000.

Zkouška
Zkouška se bude skládat z písemné a ústní části. Podrobnosti o formě zkoušky a o zkoušené látce jsou zde. Podmínkou ke zkoušce je získání zápočtu (kromě předtermínů). Zápis na zkoušku je prostřednictvím SISu.

Upozornění: Poslední dva zkouškové termíny v letním semestru jsou vypsány na 25.4. od 12:20 v S6 a 4.6. od 9:00 v S1.

Minulé zkouškové testy: Vzor, 3.1., 10.1., 15.1., 22.1., 24.1., 29.1., 5.2., 7.2., 12.2.

Konzultační hodiny
Pátek 10:40-12:20, případně po domluvě (mailem).

Poznámka
Uvítám poznámky o nepřesnostech, chybách či překlepech v přednáškových slidech.