On combinations of local theory extensions

Abstract

In this paper we study theory extensions in which efficient reasoning is possible. We study local extensions (in which hierarchical reasoning is possible) and give several examples from computer science or mathematics in which such extensions occur in a natural way.We then identify situations in which combinations of local extensions of a theory are again local extensions of that theory. We thus obtain criteria both for recognizing wider classes of local theory extensions, and for modular reasoning in combinations of theories over non-disjoint signatures. © Springer-Verlag Berlin Heidelberg 2013.