Výroková a predikátová logika
Zimní semestr 2017/18
Předchozí verze přednášky: ZS 2016/17 CZ, ZS 2015/16 CZ, ZS 2014/15 CZ, ZS 2013/14 CZ.
Lecture in English: ZS 2017/18 EN (by Martin Pilát), ZS 2016/17 EN, ZS 2015/16 EN, ZS 2014/15 EN.
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
Úvod
- 04.10. Přednáška 1: Trocha historie, paradoxy, jazyk matematiky, rozdíl a vztah syntaxe a sémantiky, předběžnosti.
Výroková logika
- 11.10. Přednáška 2: Stromy, Königovo lemma. Základní syntax a sémantika VL, univerzálnost logických spojek, normální tvary.
- 18.10. Přednáška 3: 2-SAT a Horn-SAT, sémantika vzhledem k teorii, vlastnosti teorií, algebra výroků. Tablo metoda pro VL - úvod.
- 25.10. Přednáška 4: Tablo metoda: tablo, důkaz, systematické tablo, korektnost a úplnost.
- 01.11. Přednáška 5: Kompaktnost. Rezoluční metoda: korektnost a úplnost, lineární rezoluce, rezoluce pro Prolog. Hilbertovský kalkul ve VL.
Predikátová logika
- 08.11. Přednáška odpadá (děkanský sportovní den).
- 15.11. Přednáška 6: Základní syntax PL, instance a varianty. Základní sémantika PL, struktury, platnost. Teorie, modely teorií.
- 22.11. Přednáška 7: Vlastnosti teorií. Podstruktury, otevřené teorie. Expanze, redukt, věta o konstantách. Definovatelné množiny. Booleovy algebry. Tablo metoda pro PL - úvod.
- 29.11. Přednáška 8: Tablo metoda v PL: systematické tablo, rovnost. Korektnost, kanonický model.
- 06.12. Přednáška 9: Úplnost, Löwenheim-Skolemova věta, kompaktnost. Extenze o definice. Prenexní tvar.
- 13.12. Přednáška 10: Skolemizace, Skolemova věta. Herbrandova věta. Rezoluční metoda v PL - úvod.
- 20.12. Přednáška 11: Rezoluce v PL: unifikace, korektnost a úplnost, lineární rezoluce a LI-rezoluce.
Teorie modelů. Nerozhodnutelnost, neúplnost
- 03.01. Přednáška 12: Hilbertovský kalkul v PL. Elementární ekvivalence, kompletnost. Isomorfismus struktur, kategoričnost.
- 10.01. Přednáška 13: Konečná a otevřená axiomatizovatelnost. Rozhodnutelné teorie, rekurzivní axiomatizovatelnost. Aritmetické teorie. 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.
- W. Rautenberg, A concise introduction to mathematical logic, Springer, 2009.
- J. Mlček, Výroková a predikátová logika, el. skripta, 2012.
- P. Štěpánek, Meze formální metody, el. skripta, 2000.
Cvičení
Přednáška je doplněna cvičením. Informace k mnou vedenému cvičení jsou zde.
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 upřesněny 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í: V letním semestru budou pouze tři zkouškové termíny: v půlce semestru, na začátku a na konci zkouškového období v červnu.
Minulé zkouškové testy: 9.1., 16.1., 23.1., 25.1., 31.1., 1.2., 7.2., 9.2., 13.2., 15.2.
Konzultace
Po domluvě mailem kdykoliv.
Poznámka
Uvítám poznámky o nepřesnostech, chybách či překlepech v přednáškových slidech.