Hierarchical and modular reasoning in complex theories

A long term goal of the research in computer science is the
  analysis and verification of complex systems. These can be
  theories of mathematics, programs, reactive oder hybrid systems,
  or large databases. Correctness proofs for such systems can
  often be reduced to reasoning in complex logical theories
  (e.g. combinations of numerical theories, theories of data
  types, certain theories of functions). As the resulting proof
  tasks are usually large, it is extremely important to have
  efficient decision procedures.

  In this talk we discuss situations in which efficient reasoning
  in complex theories is possible. We consider a special type of
  extensions of a base theory, which we call local extensions,
  where hierarchic reasoning is possible (i.e., we can reduce the
  task of proving satisfiability of (ground) formulae in the
  extension  to proving satisfiability of formulae in the base theory).
  We give several examples of theories important for computer
  science or mathematics which have this property. We show that the
  decidability (and complexity) of the universal fragment of a local
  theory extension can be expressed in terms of the decidability
  (resp. complexity) of a suitable fragment of the base theory.

  We briefly mention possibilities of modular reasoning in combinations
  of local theory extensions, as well as possibilities of obtaining
  interpolants in a hierarchical manner, and discuss applications in
  verification  and in knowledge representation.