Automatic Theorem Proving in Complex Theories

We identify situations in which it is possible to decompose proof tasks in complex theories in a modular way into proof tasks for the simpler components of these theories. As they exploit modularity, such proof procedures are especially flexible and efficient and are therefore widely applicable, for instance in the verification of complex systems, but also in mathematics or knowledge representation.