Viorica Sofronie-Stokkermans and Carsten Ihlemann

We give a uniform method for automated reasoning in several types of extensions of ordered algebraic structures (definitional extensions, exten-sions with boundedness axioms or with monotonicity axioms). We show that such extensions are local and, hence, efficient methods for hierarchical reasoning exist in all these cases.