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 also briefly mention possibilities of modular reasoning in combinations of local theory extensions, as well as possibilities of obtaining interpolants in a hierarchical manner, and some applications in verification and in knowledge representation.