The course is focused on practical applications of the formal apparatus of propositional as well as first-order predicate logic. This formalism is broadly used in computer science and artificial intelligence for a rigorous specification of intuitive knowledge and of particular theories, for automatic theorem proving, and many other areas. The course is focused in particular on the principles of knowledge specification and a formal specification of a software system, as well as logic programming. The students will also get acquainted with the principles of logic programming, as well as with practical applications of non-classical logics, in particular fuzzy logic.