Mathematical Logic
Code  Completion  Credits  Range  Language 

BIKMLO  Z,ZK  5  13KP+4KC  Czech 
 Lecturer:
 Karel Klouda (guarantor)
 Tutor:
 Karel Klouda (guarantor)
 Supervisor:
 Department of Applied Mathematics
 Synopsis:

Students have knowledge of the syntax and semantics of the propositional and predicate logic. They master the Boolean algebra, both theoretically as an instance of universal algebra, and practically as a tool to describe the world of digital systems. They get skills to handle Boolean functions, normal forms, maps, and minimisation methods needed in the further modules.
 Requirements:
 Syllabus of lectures:

1. Informal logic as the language of mathematics. Ambiguity of natural languages. Languages nad metalanguages. Formal languages. Language of propositional logic, syntax and semantics. Truth tables, time complexity of their processing.
2. Semantic consequence and semantic equivalence. Lindenbaum algebra of propositional logic formulas. Boolean algebra. CNF and DNF. Karnaugh maps. Boolean function minimization.
3. Basic concepts of the resolution algorithm in propositional logic. Formalizing natural language sentences, inadequacy of propositional logic. Syntax of predicate logic.
4. Semantics of predicate logic. Construction of simple models in predicate logic language.
5. Semantic consequence in predicate logic. Satisfiability. Semantic consequence problem, algorithmic point of view.
6. Formalizing natural language sentences in predicate logic. Syntactic derivation in propositional and predicate logic. Construction of successful tableaus.
7. Other logics used in CS.
 Syllabus of tutorials:

1. Formalization of simple statements. Truth tables, time complexity of their processing. Semantic consequence and semantic equivalence. CNF and DNF. Syntax and semantic of predicate logic. Resolution method in propositional logic.
2. Formalization of natural language sentences. Syntax of predicate logic. Semantic of predicate logic. Construction of simple models in predicate logic language. Semantic consequence in predicate logic. Satisfiability. Semantic consequence problem, algorithmic point of view. Proofs in propositional and predicate logic. Tableau method.
 Study Objective:
 Study materials:
 Note:
 Further information:
 https://courses.fit.cvut.cz/BIMLO/
 Timetable for winter semester 2020/2021:
 Timetable is not available yet
 Timetable for summer semester 2020/2021:
 Timetable is not available yet
 The course is a part of the following study plans:

 Bachelor program Informatics, unspecified branch, in Czech, parttime, 2015–2021 (compulsory course in the program)
 Bachelor branch Security and Information Technology, in Czech, parttime, 2015–2019 (compulsory course in the program)
 Bachelor branch Web and Software Engineering, spec. Software Engin., in Czech, parttime, 2015–2020 (compulsory course in the program)
 Bachelor branch Security and Information Technology, parttime, in Czech, 2020 (compulsory course in the program)