Detail předmětu

Pokročilá matematika

FIT-IAMAk. rok: 2017/2018

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

čeština

Počet kreditů

5

Garant předmětu

doc. Mgr. Lukáš Holík, Ph.D.

Zajišťuje ústav

Ústav inteligentních systémů (UITS)

Výsledky učení předmětu

Schopnost matematické formulace, řešení problémů pomocí matematického aparátu, zejména dokazování, prohloubení a procvičení základních matematických pojmů, přehled o některých pro informatiku stěžejních oblastech matematiky a jejich aplikacích v informatice.

Rozvinutí schopnosti exaktně se vyjadřovat a používat matematický aparát.

Prerekvizity

Základní pojmy o relacích, množinách, základy výrokové a predikátové logiky, základy algebry, základy konečných automatů.

Způsob a kritéria hodnocení

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ů).

Osnovy výuky

    Osnova přednášek:
    1. Teorie čísel: prvočísla, dělitělnost, kongruence, Fundamentální věta aritmetiky, Malá Fermatova věta, Eulerova funkce. (Dana Hliněná)
    2. Aplikace teorie čísel v kryptografii. (Dana Hliněná)
    3. Axiomy teorie množin, axiom výběru. Spočetné a nespočetné množiny, kardinální čísla. (Dana Hliněná)
    4. 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)
    5. 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)
    6. Predikátová logika. Craigova interpolace. Důležité teorie. Nerozhodnutelnost. Predikátová logika vyššího řádu. (Ondřej Lengál)
    7. Hoarova logika. Precondition, postcondition. Invariant. Deduktivní verifikace programů. (Ondřej Lengál)
    8. Logické rozhodovací procedury: Presburgerova aritmetika, teorie rekurzivních datových struktur, teorie reálných čísel. (Lukáš Holík)
    9. Částečné uspořádání a svazy, věty o pevných bodech, Knaster-Tarski a Kleene, Kleeneho iterace, WQO, chaotická iterace. (Lukáš Holík)
    10. Galoisovo spojení, abstraktní interpretace, aplikace ve verifikaci. (Lukáš Holík)
    11. Pokročilá kombinatorika: Princip inkluze a exkluze, Dirichletův princip, vybrané kombinatorické teorémy. (Milan Češka)
    12. Podmíněná pravděpodobnost, základy statistické inference, Bayesovské sítě. (Milan Češka)
    13. Náhodné procesy: Markovův a Poissonův process. Aplikace v informatice: kvantitativní analýza, analýza výkonnosti. (Milan Češka)

    Osnova numerických cvičení:
    1. Důkazové úlohy v teorii čísel, Čínská věta o zbytcích.
    2. Prvočísla a kryptografie, RSA a DSA šifry.
    3. Důkazy v teorii množin, Cantorova diagonalizace, párování, Hilbertův hotel.
    4. Důkazové metody pro výrokovou logiku.
    5. Důkazové metody pro predikátovou logiku.
    6. Rozhodovací procedury.
    7. Počítačové cvičení 1.
    8. Počítačové cvičení 2.
    9. Základy svazů a uspořádání, úlohy na výpočet pevného bodu.
    10. Počítačové cvičení 3.
    11. Důkazové metody v kombinatorice.
    12. Podmíněná pravděpodobnost v praxi, použití statistické inference.
    13. Počítačové cvičení 4.

    Osnova počítačových cvičení:
    1. Důkazy korektnosti programů v systému VCC.
    2. Solvery - SAT, SMT, MONA, Vampire.
    3. Návrh abstraktní domény, ukázka nástrojů pro abstraktní interpretaci.
    4. Analýza pravděpodobnostních systémů, nástroj PRISM.

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.

Vymezení kontrolované výuky a způsob jejího provádění a formy nahrazování zameškané výuky

Dva testy - v polovině a v závěru semestru (25 bodů za test), aktivita na cvičeních (5 bodů za každé cvičení).

Prerekvizity a korekvizity

Základní literatura

A.R. Bradley, Z. Manna. The Calculus of Computation. Springer, 2007.
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

R. Smullyan. First-Order Logic. Dover, 1995.

Zařazení předmětu ve studijních plánech

  • Program IT-BC-3 bakalářský

    obor BIT , 2 ročník, letní semestr, volitelný

Typ (způsob) výuky

 

Přednáška

26 hod., nepovinná

Vyučující / Lektor

doc. Mgr. Lukáš Holík, Ph.D.

Osnova

  1. Teorie čísel: prvočísla, dělitělnost, kongruence, Fundamentální věta aritmetiky, Malá Fermatova věta, Eulerova funkce. (Dana Hliněná)
  2. Aplikace teorie čísel v kryptografii. (Dana Hliněná)
  3. Axiomy teorie množin, axiom výběru. Spočetné a nespočetné množiny, kardinální čísla. (Dana Hliněná)
  4. 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)
  5. 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)
  6. Predikátová logika. Craigova interpolace. Důležité teorie. Nerozhodnutelnost. Predikátová logika vyššího řádu. (Ondřej Lengál)
  7. Hoarova logika. Precondition, postcondition. Invariant. Deduktivní verifikace programů. (Ondřej Lengál)
  8. Logické rozhodovací procedury: Presburgerova aritmetika, teorie rekurzivních datových struktur, teorie reálných čísel. (Lukáš Holík)
  9. Částečné uspořádání a svazy, věty o pevných bodech, Knaster-Tarski a Kleene, Kleeneho iterace, WQO, chaotická iterace. (Lukáš Holík)
  10. Galoisovo spojení, abstraktní interpretace, aplikace ve verifikaci. (Lukáš Holík)
  11. Pokročilá kombinatorika: Princip inkluze a exkluze, Dirichletův princip, vybrané kombinatorické teorémy. (Milan Češka)
  12. Podmíněná pravděpodobnost, základy statistické inference, Bayesovské sítě. (Milan Češka)
  13. Náhodné procesy: Markovův a Poissonův process. Aplikace v informatice: kvantitativní analýza, analýza výkonnosti. (Milan Češka)

Cvičení odborného základu

18 hod., povinná

Vyučující / Lektor

doc. Mgr. Lukáš Holík, Ph.D.

Osnova

  1. Důkazové úlohy v teorii čísel, Čínská věta o zbytcích.
  2. Prvočísla a kryptografie, RSA a DSA šifry.
  3. Důkazy v teorii množin, Cantorova diagonalizace, párování, Hilbertův hotel.
  4. Důkazové metody pro výrokovou logiku.
  5. Důkazové metody pro predikátovou logiku.
  6. Rozhodovací procedury.
  7. Počítačové cvičení 1.
  8. Počítačové cvičení 2.
  9. Základy svazů a uspořádání, úlohy na výpočet pevného bodu.
  10. Počítačové cvičení 3.
  11. Důkazové metody v kombinatorice.
  12. Podmíněná pravděpodobnost v praxi, použití statistické inference.
  13. Počítačové cvičení 4.

Cvičení na počítači

8 hod., nepovinná

Vyučující / Lektor

doc. Mgr. Lukáš Holík, Ph.D.

Osnova

  1. Důkazy korektnosti programů v systému VCC.
  2. Solvery - SAT, SMT, MONA, Vampire.
  3. Návrh abstraktní domény, ukázka nástrojů pro abstraktní interpretaci.
  4. Analýza pravděpodobnostních systémů, nástroj PRISM.