Detail předmětu
Pokročilá matematika
FIT-IAMAk. rok: 2020/2021
Předmět navazuje na povinné matematické předměty bakalářského studia. Práce s matematickým aparátem je demonstrována spolu s prohloubením znalostí oblastí matematiky úzce souvisejících s informatikou a s ukázkou jejich aplikací v informatice. Jedná se zejména o teorii čísel a její aplikaci v kryptografii; základy teorie množin a logiky, vybrané logické systémy, techniky a rozhodovací procedury s aplikací např. v databázích či softwarovém inženýrství; teorii svazů, pevných bodů, a jejich aplikace ve verifikaci; pravděpodobnost a statistiku a aplikace v analýze pravděpodobnostních systémů a umělé inteligenci.
Jazyk výuky
Počet kreditů
Garant předmětu
Zajišťuje ústav
Výsledky učení předmětu
Rozvinutí schopnosti exaktně se vyjadřovat a používat matematický aparát.
Prerekvizity
Způsob a kritéria hodnocení
Podmínky zápočtu:
Získání 50 ze 100 možných bodů, udělovaných za aktivity v průběhu cvičení a docházku (50 bodů), průběžné testy (50 bodů).
Učební cíle
- Prohloubit schopnosti aplikace matematického aparátu ve vyjadřování, formulaci a řešení problémů a posílit schopnosti exaktního vyjadřování a myšlení obecně,
- rozvinout některé partie matematiky s těsnou vazbou na informatiku a ukázat souvislost s informatikou,
- usnadnit studium matematických předmětů v navazujícím magisterském studiu,
- přesvědčit se na vlastní oči, jak komplikovaná matematika může vést k velmi užitečným algoritmům a nástrojům.
Prerekvizity a korekvizity
- doporučená prerekvizita
Formální jazyky a překladače - doporučená prerekvizita
Matematická analýza 1 - doporučená prerekvizita
Diskrétní matematika - doporučená prerekvizita
Matematická analýza 2 - doporučená prerekvizita
Pravděpodobnost a statistika
Základní literatura
D. P. Bertsekas, J. N. Tsitsiklis. Introduction to Probability, Athena Scientific, 2008.
M. Huth, M. Ryan. Logic in Computer Science. Modelling and Reasoning about Systems. Cambridge University Press, 2004.
Doporučená literatura
B. Balcar, P. Štěpánek. Teorie množin. Academia, 2005.
C. M. Grinstead, J. L. Snell. Introduction to probability. American Mathematical Soc., 2012.
G. Chartrand, A. D. Polimeni, P. Zhang. Mathematical Proofs: A Transition to Advanced Mathematics, 2013
R. Smullyan. First-Order Logic. Dover, 1995.
Steven Roman. Lattices and Ordered Sets, Springer-Verlag New York, 2008.
Elearning
Zařazení předmětu ve studijních plánech
Typ (způsob) výuky
Přednáška
Vyučující / Lektor
Osnova
- Axiomy teorie množin, axiom výběru. Spočetné a nespočetné množiny, kardinální čísla. (Dana Hliněná)
- Aplikace teorie čísel v kryptografii. (Dana Hliněná)
- Teorie čísel: prvočísla, dělitelnost, kongruence, Fundamentální věta aritmetiky, Malá Fermatova věta, Eulerova funkce. (Dana Hliněná)
- Výroková logika. Syntaxe, sémantika. Důkazové metody pro výrokovou logiku: metoda sémantických tabulek, přirozená dedukce, rezoluce. (Ondřej Lengál)
- Predikátová logika. Syntaxe, sémantika prvořádové predikátové logiky. Důkazové metody pro predikátovou logiku: metoda sémantických tabulek, přirozená dedukce. (Ondřej Lengál)
- Predikátová logika. Craigova interpolace. Důležité teorie. Nerozhodnutelnost. Predikátová logika vyššího řádu. (Ondřej Lengál)
- Hoarova logika. Precondition, postcondition. Invariant. Deduktivní verifikace programů. (Ondřej Lengál)
- Logické rozhodovací procedury: Klasické rozhodovací procedury pro aritmetiku nad celými a racionálními čísly. (Lukáš Holík)
- Automatové rozhodovací procedury pro aritmetiku a WS1S. (Lukáš Holík)
- Rozhodovací procedury pro kombinované teorie. (Lukáš Holík)
- Stochastické procesy. Modelování pravděpodobnostních systémů pomocí Markovských řetězců diskrétního času. (Milan Češka)
- Analýza Markovských řetězců (model checking). Demonstrace nástroje PRISM. (Milan Češka)
- Rozšíření Markovských řetězců o nedeterminismus, Markovské řetězce ve spojitém čase. Skryté Markovské řetězce. (Milan Češka)
Cvičení odborného základu
Vyučující / Lektor
Osnova
- Důkazy v teorii množin, Cantorova diagonalizace, párování, Hilbertův hotel.
- Prvočísla a kryptografie, RSA a DSA šifry.
- Důkazové úlohy v teorii čísel, Čínská věta o zbytcích.
- Důkazové metody pro výrokovou logiku.
- Důkazové metody pro predikátovou logiku.
- Rozhodovací procedury.
- Počítačové cvičení 1.
- Počítačové cvičení 2.
- Automatové rozhodovací procedury a kombinované teorie.
- Počítačové cvičení 3.
- Modelování pravděpodobnostních systémů.
- Analýza Markovských řetězců.
- Počítačové cvičení 4.
Cvičení na počítači
Vyučující / Lektor
Osnova
- Důkazy korektnosti programů v systému VCC.
- Solvery - SAT, SMT.
- Solvery - Mona, Vampire.
- Analýza pravděpodobnostních systémů pomocí nástroje PRISM.
Elearning