Výroková a predikátová logika
Zimní semestr 2020/21
Loňská verze přednášky: ZS 2019/20 CZ.
Lecture in English: ZS 2020/21 EN (by Jakub Bulín), ZS 2018/19 EN (by Martin Pilát), ZS 2016/17 EN.
Rozvrh: Pátek 10:40-12:10, Zoom link.
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 bude konat dle rozvrhu na platformě Zoom, viz link výše. Pokud jste nedostali pozvánku s heslem či máte jiné potíže s připojením, napište mi. Záznamy z přednášek budou k dispozici v playlistu na Streamu UK.
Plán přednášky
Výroková logika
- 02.10. Přednáška 1: Trocha historie, paradoxy, jazyk matematiky, základní syntax VL. Dodatek. [video01]
- 09.10. Přednáška 2: Sémantika VL, univerzálnost logických spojek, normální tvary, SAT řešiče, 2-SAT. [video02]
- 16.10. Přednáška 3: Horn-SAT. Sémantika vzhledem k teorii, vlastnosti teorií, algebra výroků. Tablo metoda pro VL - úvod. [video03]
- 23.10. Přednáška 4: Tablo metoda s axiomy, systematické tablo, korektnost a úplnost, kompaktnost. [video04]
- 30.10. Přednáška 5: Rezoluční metoda: korektnost a úplnost, lineární rezoluce, rezoluce pro Prolog. Hilbertovský kalkul ve VL. [video05]
Predikátová logika
- 06.11. Přednáška 6: Základní syntax PL, instance a varianty. Základní sémantika PL, struktury, platnost. Teorie, modely teorií. [video06]
- 23.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 - úvod. [video07]
- 20.11. Přednáška 8: Tablo metoda v PL: systematické tablo, rovnost. Korektnost. [video08]
- 27.11. Přednáška 9: Kanonický model, úplnost, Löwenheim-Skolemova věta, kompaktnost. Extenze o definice. [video09]
- 04.12. Přednáška 10: Prenexní tvar. Skolemizace, Skolemova věta. Herbrandova věta. Rezoluční metoda v PL - úvod. [video10]
- 11.12. Přednáška 11: Rezoluční metoda v PL: korektnost, úplnost, LI-rezoluce. Hilbertovský kalkul v PL. [video11]
Teorie modelů. Nerozhodnutelnost, neúplnost
- 18.12. Přednáška 12: Elementární ekvivalence, kompletnost. Isomorfismus struktur, kategoričnost. Axiomatizovatelnost. [video12]
- 08.01. Přednáška 13: Rozhodnutelné teorie, rekurzivní axiomatizovatelnost. Aritmetické teorie. Nerozhodnutelnost PL. Věty o neúplnosti, důsledky. [video13]
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. Domácí úkoly budou cvičící typicky zadávat přes Moodle.
Příklady k procvičení z minulých let jsou zde.
Zkouška
Zkouška se bude skládat z písemné a ústní části. Podrobnosti o formě zkoušky 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.
Preferovaná forma zkoušky je prezenční, ale těm, kdo se nemohou prezenční zkoušky zúčastnit nebo jen s vážnými komplikacemi (zdravotní důvody, mimo dojezdovou vzdálenost apod.) bude umožněno 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.
Důležité: Pokud se jedná o druhý opravný termín při druhém zápisu předmětu, je nutné se ke zkoušce přihlásit alespoň dva dny předem, tj. 48 hodin před začátkem zkoušky. To platí jak pro distanční, tak i prezenční zkoušky.
Nové: Poslední zkouškový termín bude v 14.9.
Pozn.: Hledám zájemce o ročníkový projekt / bakalářskou práci na generování zkouškových testů, viz podrobnosti.
Minulé zkouškové testy: 7.1. (řešení 7.1.), 14.1., 21.1., 28.1., 1.2., 9.2., 17.2., 19.2., 25.2. (řešení 25.2.), 9.6., , 1.7.
Konzultace
Po domluvě mailem či po přednášce.