Course details

Advanced Mathematics

IAM Acad. year 2016/2017 Summer semester 5 credits

Current academic year

Item has no anotation.

Guarantor

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

Language of instruction

Czech, English

Completion

Classified Credit

Time span

  • 26 hrs lectures
  • 18 hrs exercises
  • 8 hrs pc labs

Assessment points

  • 50 pts mid-term test (written part)
  • 50 pts numeric exercises

Department

Department of Intelligent Systems (UITS)

Subject specific learning outcomes and competences

Item has no knowledges.

Learning objectives

Item has no goals.

Recommended prerequisites

Prerequisite knowledge and skills

There are no prerequisites

Study literature

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

Fundamental literature

  • 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.

Syllabus of lectures

  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)

Syllabus of numerical exercises

  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.

Syllabus of computer exercises

  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.

Progress assessment

Výuka není kontrolována.

Controlled instruction

There are no checked study.

Back to top