A long term goal of the research in computer science is the analysis and verification of complex systems (these can for instance be programs, reactive or hybrid systems, large databases). In many cases, correctness proofs for such systems can be reduced to reasoning in complex logical theories (for instance, combinations of numerical theories and theories of data types, or certain theories of continuous and/or derivable functions). As the resulting proof tasks are usually large, it is extremely important to have efficient decision procedures for such complex theories.

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 which have this property. We also briefly mention possibilities of modular reasoning in combinations of local theory extensions, and some applications in the verification of parametric systems.