Detail předmětu
Základy logiky pro informatiky
IZLO Ak. rok 2024/2025 letní semestr 2 kredity
Formální výroková a predikátová logika. Syntaxe a sémantika formulí. Normální formy a algebraické úpravy formulí. Formální důkaz jako sekvence aplikací syntaktických pravidel vycházející z axiomů. Prvořádové teorie, modely. Pojmy korektnost, bezespornost, úplnost. Praktické použití SAT a SMT solverů. Souvislost dokazování a počítání, existence limitů dokazování a počítání plynoucí z Gödelových vět.
Garant předmětu
Koordinátor předmětu
Jazyk výuky
Zakončení
Rozsah
- 10 hod. přednášky
- 2 hod. seminář
- 10 hod. cvičení
- 2 hod. projekty
Bodové hodnocení
- 82 bodů závěrečná zkouška
- 18 bodů projekty
Zajišťuje ústav
Přednášející
Cvičící
Holík Lukáš, doc. Mgr., Ph.D.
Chocholatý David, Ing. (UITS)
Kocourek Tomáš, Ing. (UITS)
Lengál Ondřej, Ing., Ph.D. (UITS)
Síč Juraj, Mgr. (UITS)
Cíle předmětu
Seznámení s nejzákladnějšími pojmy, koncepty a výsledky klasické matematické logiky (související se syntaxí, sémantikou a dokazováním ve výrokové a predikátové logice); nacvičení formálního vyjadřování pomocí aparátu matematické logiky; uvedení do souvislostí počítání, formálního logického usuzování a jejich limitů; seznámení s praktickými technologiemi automatického logického usuzování - SAT a SMT solving.
Orientace v pojmech matematické logiky jako term, formule, axiom, důkaz, syntaxe, sémantika, splnitelnost, platnost, korektnost, spornost, úplnost, axiom, důkaz. Schopnost práce s jazykem výrokové a predikátové logiky: důkladné porozumění významu a použití symbolům výrokové a predikátové logiky, spojek, kvantifikátorů, logických proměnných. Schopnost psát a číst texty s prvky formální notace. Zlepšení celkové schopnosti formálního a přesného vyjadřování a myšlení. Základní znalost nejzásadnějších výsledků v matematické logice, Gödelových vět, a jejich významu pro informatiku. Povědomí o praktickém užití SAT a SMT solverů.
Doporučené prerekvizity
- Diskrétní matematika (IDM)
Požadované prerekvizitní znalosti a dovednosti
Základy diskrétní matematiky a matematické notace, množiny, relace, zobrazení.
Literatura studijní
- Herbert B. Enderton. A Mathematical Introduction to Logic. Academic Press, 2001. ISBN 978-0122384523
Literatura referenční
- Herbert B. Enderton. A Mathematical Introduction to Logic. Academic Press, 2001. ISBN 978-0122384523
- Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, 2004. ISBN 978-0521543101
- Peter Smith. An Introduction to Formal Logic. ISBN 978-1916906327 https://www.logicmatters.net/ifl/
- Peter Smith. Gödel Without (Too Many) Tears. ISBN 979-8673862131 https://www.logicmatters.net/igt/
- Doxiadis A, Papadimitriou C. LOGICOMIX: an epic search for truth. Bloomsbury Publishing USA; 2015 Jul 28. ISBN 978-1596914520
Osnova přednášek
- Úvod, syntaxe a sémantika výrokové logiky, splnitelnost, platnost, tabulky, konjunktivní a disjunktivní normální forma, algebraické úpravy formulí, úplné systémy spojek.
- Syntaxe a sémantika predikátové logiky.
- Normální formy a algebraické úpravy predikátových formulí. Teorie v predikátové logice.
- Dokazování. Důkaz z axiomů pomocí odvozovacích pravidel. Vztah syntaxe a sémantiky. Efektivní, korektní, úplný dokazovací systém.
- Bezespornost a úplnost prvořádových teorií. Vztah počítání a dokazování, mechanizovatelnost matematiky a teorií PL, Gödelovy věty o neúplnosti.
Osnova seminářů
- SAT a SMT solving.
Osnova cvičení
- Výroková logika: formalizace tvrzení, splňování formulí, tabulky, převody do CNF a DNF.
- Predikátová logika: kvantifikátory a proměnné. Formalizace a porozumění formulím 1.
- Predikátová logika: interpretace jazyka, model formule. Formalizace a porozumění formulím 2.
- Algebraické úpravy a převody do normálních forem.
- Dokazování.
Osnova ostatní - projekty, práce
- Použití SAT solverů
- Použití SMT solverů
Průběžná kontrola studia
Hodnocení projektu, který se bude skládat ze dvou příkladů: 1) použití SAT solveru, 2) použití SMT solveru.
Projekt hodnocený max. 20 body, písemná zkouška max. 80 body. Pro úspěšné absolvování předmětu je třeba získat alespoň 50 bodů celkem ze 100 a polovinu bodů ze zkoušky (t.j. 40 bodů z 80).
Rozvrh
Den | Typ | Týdny | Místn. | Od | Do | Kapacita | PSK | Skup | Info |
---|---|---|---|---|---|---|---|---|---|
Po | cvičení | 1., 8., 9., 10., 12., 13. výuky | A112 A113 | 14:00 | 15:50 | 50 | 1BIA 1BIB 2BIA 2BIB | xx | |
Po | cvičení | 2., 3., 4., 5., 6. výuky | A112 | 14:00 | 15:50 | 50 | 1BIA 1BIB 2BIA 2BIB | xx | Chocholatý |
Po | cvičení | 2., 3., 4., 5., 6. výuky | A113 | 14:00 | 15:50 | 50 | 1BIA 1BIB 2BIA 2BIB | xx | Kocourek |
Po | přednáška | 1., 2., 3. výuky | E104 E105 E112 | 16:00 | 17:50 | 294 | 1BIB 2BIA 2BIB | 30 - 49 xx | Lengál |
Po | přednáška | 4., 5. výuky | E104 E105 E112 | 16:00 | 17:50 | 294 | 1BIB 2BIA 2BIB | 30 - 49 xx | Holík |
Út | cvičení *) | 4., 5., 6., 7., 8., 9., 10., 11., 12., 13. výuky | A112 | 13:00 | 14:50 | 64 | 1BIA 1BIB 2BIA 2BIB | xx | |
Út | přednáška | 1., 2., 3. výuky | D0206 D105 | 15:00 | 16:50 | 470 | 1BIA 2BIA 2BIB | 10 - 29 xx | Lengál |
Út | přednáška | 4., 5. výuky | D0206 D105 | 15:00 | 16:50 | 470 | 1BIA 2BIA 2BIB | 10 - 29 xx | Holík |
St | cvičení | 2., 3., 4., 5., 6., 8., 9., 10., 11., 12., 13. výuky | A112 | 08:00 | 09:50 | 50 | 1BIA 1BIB 2BIA 2BIB | xx | Hečko |
St | cvičení | 2., 3., 4., 5., 6., 8., 9., 10., 11., 12., 13. výuky | D0207 | 08:00 | 09:50 | 50 | 1BIA 1BIB 2BIA 2BIB | xx | Chocholatý |
St | cvičení | 2., 3., 4., 5., 6., 8., 9., 10., 11., 12., 13. výuky | A112 | 14:00 | 15:50 | 50 | 1BIA 1BIB 2BIA 2BIB | xx | Lengál |
St | cvičení | 2., 3., 4., 5., 6., 8., 9., 10., 11., 12., 13. výuky | A113 | 14:00 | 15:50 | 50 | 1BIA 1BIB 2BIA 2BIB | xx | Hečko |
St | cvičení | 2., 3., 4., 5., 6., 8., 9., 10., 11., 12., 13. výuky | D0207 | 14:00 | 15:50 | 50 | 1BIA 1BIB 2BIA 2BIB | xx | Chocholatý |
St | cvičení *) | 4., 5., 6., 7., 8., 9., 10., 11., 12., 13. výuky | A112 | 16:00 | 17:50 | 64 | 1BIA 1BIB 2BIA 2BIB | xx | |
Čt | cvičení | 2., 3., 4., 5., 6., 8., 9., 10., 11. výuky | A112 | 08:00 | 09:50 | 50 | 1BIA 1BIB 2BIA 2BIB | xx | Lengál |
Čt | cvičení | 2., 3., 4., 5., 6., 8., 9., 10., 11. výuky | D0207 | 08:00 | 09:50 | 50 | 1BIA 1BIB 2BIA 2BIB | xx | Kocourek |
Čt | cvičení | 2., 3., 4., 5., 6., 8., 9., 10., 11. výuky | G202 | 08:00 | 09:50 | 50 | 1BIA 1BIB 2BIA 2BIB | xx | Síč |
Čt | cvičení | 2., 3., 4., 5., 6., 8., 9., 10., 11. výuky | D0207 | 10:00 | 11:50 | 50 | 1BIA 1BIB 2BIA 2BIB | xx | Kocourek |
Čt | cvičení | 2., 3., 4., 5., 6., 8., 9., 10., 11. výuky | G202 | 10:00 | 11:50 | 50 | 1BIA 1BIB 2BIA 2BIB | xx | Síč |
Pá | cvičení *) | 4., 5., 6., 7., 8., 9., 11., 12., 13. výuky | A112 | 08:00 | 09:50 | 50 | 1BIA 1BIB 2BIA 2BIB | xx | |
Pá | cvičení *) | 4., 5., 6., 7., 8., 9., 11., 12., 13. výuky | A112 | 10:00 | 11:50 | 64 | 1BIA 1BIB 2BIA 2BIB | xx |
Zařazení předmětu ve studijních plánech
- Program BIT, 1. ročník, povinný
- Program BIT (anglicky), 1. ročník, povinný