Výroková a predikátová logika

Předchozí verze přednášky: ZS 2017/18 CZ, ZS 2016/17 CZ, ZS 2015/16 CZ, ZS 2014/15 CZ, ZS 2013/14 CZ.
Lecture in English: ZS 2018/19 EN (by Martin Pilát), ZS 2016/17 EN, ZS 2015/16 EN, ZS 2014/15 EN.

Rozvrh: Pátek 10:40-12:10, posluchárna S5.
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
• 05.10. Přednáška 1: Trocha historie, paradoxy, jazyk matematiky, rozdíl a vztah syntaxe a sémantiky, předběžnosti, Königovo lemma.

Výroková logika
• 12.10. Přednáška 2: Základní syntax a sémantika VL, univerzálnost logických spojek, normální tvary, SAT řešiče, 2-SAT.
• 19.10. Přednáška 3: Horn-SAT. Sémantika vzhledem k teorii, vlastnosti teorií, algebra výroků. Tablo metoda pro VL - úvod.
• 26.10. Přednáška 4: Tablo metoda s axiomy, systematické tablo, korektnost a úplnost, kompaktnost.
• 02.11. Přednáška 5: Rezoluční metoda: korektnost a úplnost, lineární rezoluce, rezoluce pro Prolog. Hilbertovský kalkul ve VL.

Predikátová logika
• 09.11. Přednáška 6: Základní syntax PL, instance a varianty. Základní sémantika PL, struktury, platnost při ohodnocení.
• 16.11. Přednáška 7: Teorie, modely teorií, vlastnosti teorií. Podstruktury, otevřené teorie. Expanze, redukt, věta o konstantách. Definovatelné množiny. Booleovy algebry.
• 23.11. Přednáška 8: Tablo metoda v PL, systematické tablo, rovnost. Korektnost.
• 30.11. Přednáška 9: Kanonický model, úplnost, Löwenheim-Skolemova věta, kompaktnost.
• 07.12. Přednáška 10: Extenze o definice. Prenexní tvar. Skolemizace, Skolemova věta. Herbrandova věta.
• 14.12. Přednáška 11: Rezoluční metoda v PL: úvod, unifikace, korektnost.

Teorie modelů. Nerozhodnutelnost, neúplnost
• 21.12. Přednáška 12: Rezoluce: úplnost, LI-rezoluce. Hilbertovský kalkul v PL. Elementární ekvivalence, kompletnost.
• 04.01. Přednáška 13: Isomorfismus struktur, kategoričnost. Konečná a otevřená axiomatizovatelnost.
• 11.01. Přednáška 14: 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.

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. Na stránkách z minulých let jsou zveřejněny dřívější zkušební testy.

Upozornění: V letním semestru budou pouze tři zkouškové termíny: v půlce semestru 17.4., na začátku 30.5. a na konci zkouškového období v červnu 26.6.

Minulé zkouškové testy: 8.1., 15.1., 17.1., 21.1., 23.1., 29.1., 1.2., 8.2., 12.2., 14.2.

Konzultace
Po domluvě mailem.