Detail předmětu
Základy logiky pro informatiky
FIT-IZLOAk. rok: 2022/2023
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.
Jazyk výuky
čeština
Počet kreditů
2
Garant předmětu
Zajišťuje ústav
Výsledky učení předmětu
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ů.
Prerekvizity
Základy diskrétní matematiky a matematické notace, množiny, relace, zobrazení.
Způsob a kritéria hodnocení
Hodnocení projektu, který se bude skládat ze dvou příkladů: 1) použití SAT solveru, 2) použití SMT solveru.
Učební cíle
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.
Vymezení kontrolované výuky a způsob jejího provádění a formy nahrazování zameškané výuky
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).
Prerekvizity a korekvizity
- povinná prerekvizita
Diskrétní matematika
Základní literatura
Doxiadis A, Papadimitriou C. LOGICOMIX: an epic search for truth. Bloomsbury Publishing USA; 2015 Jul 28. ISBN 978-1596914520 (EN)
Doxiadis A, Papadimitriou C. LOGICOMIX: an epic search for truth. Bloomsbury Publishing USA; 2015 Jul 28. ISBN 978-1596914520 (CS)
Herbert B. Enderton. A Mathematical Introduction to Logic. Academic Press, 2001. ISBN 978-0122384523 (CS)
Herbert B. Enderton. A Mathematical Introduction to Logic. Academic Press, 2001. ISBN 978-0122384523 (EN)
Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, 2004. ISBN 978-0521543101 (EN)
Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, 2004. ISBN 978-0521543101 (CS)
Peter Smith. An Introduction to Formal Logic. ISBN 978-1916906327 https://www.logicmatters.net/ifl/ (CS)
Peter Smith. An Introduction to Formal Logic. ISBN 978-1916906327 https://www.logicmatters.net/ifl/ (EN)
Peter Smith. Gödel Without (Too Many) Tears. ISBN 979-8673862131 https://www.logicmatters.net/igt/ (CS)
Peter Smith. Gödel Without (Too Many) Tears. ISBN 979-8673862131 https://www.logicmatters.net/igt/ (EN)
Doxiadis A, Papadimitriou C. LOGICOMIX: an epic search for truth. Bloomsbury Publishing USA; 2015 Jul 28. ISBN 978-1596914520 (CS)
Herbert B. Enderton. A Mathematical Introduction to Logic. Academic Press, 2001. ISBN 978-0122384523 (CS)
Herbert B. Enderton. A Mathematical Introduction to Logic. Academic Press, 2001. ISBN 978-0122384523 (EN)
Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, 2004. ISBN 978-0521543101 (EN)
Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, 2004. ISBN 978-0521543101 (CS)
Peter Smith. An Introduction to Formal Logic. ISBN 978-1916906327 https://www.logicmatters.net/ifl/ (CS)
Peter Smith. An Introduction to Formal Logic. ISBN 978-1916906327 https://www.logicmatters.net/ifl/ (EN)
Peter Smith. Gödel Without (Too Many) Tears. ISBN 979-8673862131 https://www.logicmatters.net/igt/ (CS)
Peter Smith. Gödel Without (Too Many) Tears. ISBN 979-8673862131 https://www.logicmatters.net/igt/ (EN)
Doporučená literatura
Herbert B. Enderton. A Mathematical Introduction to Logic. Academic Press, 2001. ISBN 978-0122384523 (EN)
Herbert B. Enderton. A Mathematical Introduction to Logic. Academic Press, 2001. ISBN 978-0122384523 (CS)
Herbert B. Enderton. A Mathematical Introduction to Logic. Academic Press, 2001. ISBN 978-0122384523 (CS)
Elearning
eLearning: aktuální otevřený kurz
Zařazení předmětu ve studijních plánech
Typ (způsob) výuky
Přednáška
10 hod., nepovinná
Vyučující / Lektor
Osnova
- Ú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.
Cvičení odborného základu
2 hod., nepovinná
Vyučující / Lektor
Osnova
- SAT a SMT solving
Cvičení
10 hod., nepovinná
Vyučující / Lektor
Osnova
- 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í.
Projekt
2 hod., nepovinná
Vyučující / Lektor
Osnova
- Použití SAT solverů
- Použití SMT solverů
Elearning
eLearning: aktuální otevřený kurz