Techniques in computer mathematics can be roughly divided into deduction and computation. This subject is about deduction. Students shall learn about advanced computational techniques based on logic inference or formal methods and the role they play in theoretical computer science. Besides getting familiar with the most important ideas in the area, students shall also be brought into a position to develop reasoning systems on their own, be able analyze their power, and understand their inherent limitations.
Subject
The courses Automated Deduction and SAT Solving are continuations of the course Computational Logic of the bachelor curriculum Technical Mathematics. Automated Deduction has its focus on predicate logic while SAT Solving is about propositional logic. The course Mathematical Logic is an introduction to classical (formal) logic, and the course on Manyvalued Logic addresses theories with more than two truth values, an important area of non-classical logic.
