Enabling students to develop abstract and formal thinking and to acquire basic knowledge in the field of mathematical logic with application in computer science.

Acquiring knowledge related to basic notions and results in the field of mathematical logic. Ability to use the acquired knowledge and skills in further education and practice.

1) Basic notions of the syntax of logical systems. 2) Classical logic. Intuitionistic logic. Propositional calculus. 3) Axiomatic system, natural deduction, sequent calculus. 4) Basic notions of the syntax of predicate calculus. 5) Basic notions of the semantics of logical systems. DPLL procedure, the tableaux method, the resolution method. 6) Computational interpretation of logic: lambda calculus and the theory of combinators. Untyped and simply-typed calculus. Curry-Howard correspondence (formulae-as-types, proofs-as-terms) between logical systems, the lambda calculus and the theory of combinators.

The theoretical part of the course is taught in lectures followed by typical examples for better understanding. Exercises, which accompanies lectures, provide typical problems and their solutions which will deepen the knowledge from the lectures. Besides lectures and exercises, consultations with professors are held on a regular basis.