IAM Acad. year 2018/2019 Summer semester 5 credits
Language of instruction
Course Web Pages
Subject specific learning outcomes and competences
Generic learning outcomes and competences
- Practice mathematical writing and thinking, formulation of problems and solving them,
- obtain deeper insight into several areas of mathematics with applications in computer science,
- learn on examples that complicated mathematics can lead to useful algorithms and tools.
Why is the course taught
- Discrete Mathematics (IDA)
Prerequisite kwnowledge and skills
- R. Smullyan. First-Order Logic. Dover, 1995.
- 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
- J. Hromkovič. Algorithmic adventures: from knowledge to magic. Dordrecht: Springer, 2009.
- Steven Roman. Lattices and Ordered Sets, Springer-Verlag New York, 2008.
- A. Doxiadis, C. Papadimitriou. Logicomix: An Epic Search for Truth. Bloomsbury, 2009.
- A.R. Bradley, Z. Manna. The Calculus of Computation. Springer, 2007.
- D. P. Bertsekas, J. N. Tsitsiklis. Introduction to Probability, Athena, 2008. Scientific
- M. Huth, M. Ryan. Logic in Computer Science. Modelling and Reasoning about Systems. Cambridge University Press, 2004.
Syllabus of lectures
- Axioms of set theory, axiom of choice. Countable and uncountable sets, cardinal numbers. (Dana Hliněná)
- Application of number theory in cryptography. (Dana Hliněná)
- Number theory: prime numbers, Fermat's little theorem, Euler's function. (Dana Hliněná)
- Propositional logic. Syntax and semantics. Proof techniques for propositional logic: syntax tables, natural deduction, resolution. (Ondřej Lengál)
- Predicate logic. Syntax and semantics. Proof techniques for predicate logic: semantic tables, natural deduction. (Ondřej Lengál)
- Predicate logic. Craig interpolation. Important theories. Undecidability. Higher order logics. (Ondřej Lengál)
- Hoare logic. Precondition, postcondition. Invariant. Deductive verification of programs. (Ondřej Lengál)
- Decision procedures in logic: Classical decision procedures for arithmetics over integers and over rationals. (Lukáš Holík)
- Automata-based decision procedures for arithmetics and for WS1S (Lukáš Holík)
- Decision procedures for combined theories. (Lukáš Holík)
- Advanced combinatorics: inclusion and exclusion, Dirichlet's principle, chosen combinatorial theorems. (Milan Češka)
- Conditional probability, statistical inference, Bayesian networks. (Milan Češka)
- Probabilistic processes: Markov and Poisson process. Applications in informatics: quantitative analysis, performance analysis.
Syllabus of numerical exercises
- Proofs in set theory, Cantor's diagonalization, matching, Hilbert's hotel.
- Prime numbers and cryptography, RSA, DSA, cyphers.
- Proofs in number theory, Chinese reminder theorem.
- Proofs in propositional logic.
- Proofs in predicate logic.
- Decision procedures.
- Computer labs 1.
- Computer labs 2.
- Automata decision procedures and combination theories.
- Computer labs 3.
- Proofs in combinatorics.
- Conditional probability and statistical inference in practice.
- Computer labs 4.
Syllabus of computer exercises
- Proving programs corrects in VCC.
- SAT and SMT solvers.
- Tools MONA and Vampire.
- Analysis of probabilistic systems, PRISM.
Course inclusion in study plans