Výroková a predikátová logika

Aktuální přednáška: ZS 2022/23 CZ (Jakub Bulín).
Lecture in English: ZS 2022/23 EN

Předchozí verze přednášky: ZS 2020/21 CZ, ZS 2021/22 EN (by Jakub Bulín), ZS 2018/19 EN (by Martin Pilát).

Rozvrh: Úterý 15:40-17:10, posluchárna M1, Ke Karlovu 3.
Přednášející: Petr Gregor (gregor(at)ktiml.mff.cuni.cz)
Informace k přednášce: 2/2 Zk/Z NAIL062 v SISu

Oznámení: Přednáška se nebude nahrávat, ale k dispozici jsou záznamy přednášek z minulého roku v playlistu na Streamu UK a v SISu.

Plán přednášky

Výroková logika
• 05.10. Přednáška 1: Úvod, trocha historie, paradoxy, jazyk matematiky. Dodatek.
• 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, Horn-SAT.
• 19.10. Přednáška 3: Sémantika vzhledem k teorii, vlastnosti teorií, algebra výroků. Tablo metoda pro VL.
• 26.10. Přednáška 4: Systematické tablo, korektnost a úplnost, kompaktnost. Hilbertovský kalkul ve VL.
• 02.11. Přednáška 5: Rezoluční metoda: korektnost a úplnost, lineární rezoluce, rezoluce pro Prolog.

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

Teorie modelů. Nerozhodnutelnost, neúplnost
• 21.12. Přednáška 12: Isomorfismus struktur, kategoričnost. Definovatelnost. Axiomatizovatelnost.
• 04.01. Přednáška 13: 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.


• M. Pilát, Propositional and Predicate Logic, lecture notes, 2017.
• 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 požadavcích 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, nově i řešení dvou testů z loňského roku. Ve vyjímečných případech (zdravotní důvody, lockdown, ...) umožníme zkoušku skládat distančně. Pro domluvu termínu a detailů zkoušky se obraťte mailem na kolegu Jakuba Bulína, který vede anglickou paralelku, a uveďte i důvody pro distanční zkoušku.

Minulé zkouškové testy: 5.1., 12.1., 14.1., 18.1., 20.1., 26.1., 28.1., 3.2., 7.2., 11.2., 13.4., 1.6., 29.6., 20.9.

Pozn.: Hledám zájemce o ročníkový projekt / bakalářskou práci na generování zkouškových testů, viz podrobnosti, podmínkou je úspěšné absolvování zkoušky.

Konzultace
Po domluvě mailem či po přednášce. K dispozici je i diskuzní fórum na Moodle.