Research Group 1: Automation of Logic
The research of this group concentrates on automated deduction in (subsets of) first-order logic. On the theoretical side, the work is focused on the development, analysis, and combination of logical calculi. Practically, the group is concerned with the implementation of powerful automated theorem provers and other deductive systems and their application. One central application area is computer-aided verification of hardware and software.
Research Areas
Christoph Weidenbach
First-Order Theorem Proving
Decidable Fragments
Automated Verification
Martin Bromberger
Jasmin Christian Blanchette
Thomas Sturm
Sophie Tourret
