We develop tools that allow computers to reason in a mathematically precise way, which is indispensable for the reliable design of automated systems. To this end, the group advances the state of the art in fields such as proof assistants, inductive logic programming, planning, formal verification, and SMT solvers.