Přístupnostní navigace
E-application
Search Search Close
Course detail
FIT-IZLOAcad. year: 2023/2024
Formal propositional and predicate logic. Syntax and semantics of formulae. Normal forms and algebraic manipulation with formulae. Formal proof as a sequence of applications of syntactic rules originating in axioms. First order theories, models. Notions of correctness, soundness, completeness. Usage of SAT and SMT solvers. Connections of proving and computation, existence of their limits following from Gödel's theorems.
Language of instruction
Number of ECTS credits
Mode of study
Guarantor
Department
Entry knowledge
Rules for evaluation and completion of the course
Evaluation of the project, which will consist of two homeworks: 1) use of SAT solver, 2) use of SMT solver. The project is evaluated with a maximum of 18 points, the written exam with a maximum of 82 points. For successful completion of the course, you must obtain at least 50 points out of the 100 and also 40 points from the final exam.
Aims
Study aids
Prerequisites and corequisites
Basic literature
Recommended reading
Elearning
Classification of course in study plans
branch BIT , 1 year of study, summer semester, compulsory
Lecture
Teacher / Lecturer
Syllabus
Seminar
Exercise
Project