Výroková a predikátová logika

Další verze přednášky: English version ZS 2014/15, ZS 2013/14.

Rozvrh: Středa 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
• 01.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
• 08.10. Přednáška 2: Základní syntax a sémantika VL, univerzálnost logických spojek, normální tvary, 2-SAT.
• 15.10. Přednáška 3: Horn-SAT, sémantika vzhledem k teorii, vlastnosti teorií, algebra výroků. Tablo metoda pro VL.
• 22.10. Přednáška 4: Tablo metoda: tablo z teorie, systematické tablo, korektnost a úplnost.
• 29.10. Přednáška 5: Kompaktnost. Rezoluční metoda: korektnost a úplnost, lineární rezoluce, rezoluce pro Prolog.

Predikátová logika
• 05.11. Přednáška 6: Hilbertovský kalkul ve VL. Základní syntax PL, instance a varianty. Základní sémantika PL, struktury, platnost ve struktuře.
• 12.11. Přednáška odpadá (děkanský den).
• 19.11. Přednáška 7: Platnost v teorii, model teorie. Vlastnosti teorií. Podstruktury, otevřené teorie. Expanze, redukt, věta o konstantách. Booleovy algebry. Tablo metoda pro PL - úvod.
• 26.11. Přednáška 8: Tablo metoda v PL: tablo důkaz, systematické tablo, rovnost, korektnost.
• 03.12. Přednáška 9: Úplnost, důsledky věty o úplnosti. Extenze o definice. Prenexní tvar.
• 10.12. Přednáška 10: Skolemizace, Herbrandova věta. Rezoluční metoda v PL.

Teorie modelů. Nerozhodnutelnost, neúplnost
• 17.12. Přednáška 11: Hilbertovský kalkul v PL. Elementární ekvivalence, kompletnost. Isomorfismus struktur. Konečná a otevřená axiomatizovatelnost. Základní matematické teorie. Aritmetické teorie.
• 07.01. Přednáška 12: Rozhodnutelné teorie. Rekurzivní axiomatizovatelnost. Nerozhodnutelnost PL. Věty o neúplnosti, důsledky.

Doporučená literatura

• A. Nerode, R.A. Shore, Logic for Applications, Springer, 2. vydání, 1997.
• P. Pudlák, Logical Foundations of Mathematics and Computational Complexity - A Gentle Introduction, Springer, 2013.
• V. Švejdar, Logika, neúplnost, složitost a nutnost, Academia, Praha, 2002.
• A. Sochor, Klasická matematická logika, Univerzita Karlova v Praze - Karolinum, 2001.
• 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í termíny zkoušky jsou 3. 6. a 23. 6. od 9:00 v S1, viz SIS.

Minulé zkouškové testy: 18.12., 8.1., 13.1., 20.1., 29.1., 4.2., 5.2., 10.2., 12.2..

Konzultace
Po domluvě mailem.

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