Many problems in mathematics and computer science can be reduced to proving
the satisfiability of conjunctions of literals in a background theory
which can itself be a combination of theories.
So-called local theory extensions allow for hierarchical
reasoning: A given ground satisfiability problem in the extended
setting is effectively reduced to an equi-satisfiable problem over the
base theory.
In this thesis, the theory of local extensions is developed and some
applications are given. Further, the theory of local theory
extensions is generalized in order to deal with data structures that
exhibit local behavior: A suitable fragment of
both the theory of arrays and the theory of pointers is local in this
broader sense. Finally, the case of more than one theory extension is
discussed. In
particular, a modularity result is given that under certain
circumstances the locality of each of the extensions lifts to locality
of the entire extension.