Equivalence of Shiny and Strongly Polite Theories
Filipe Casal · 2014
In this paper we show that a many-sorted shiny theory with respect to a set of sorts is strongly polite with respect to that set, and vice-versa, assuming that the theory has a decidable quantier-free satisability problem. Moreover, we provide sucient conditions for a many-sorted polite theory with respect to the set of all sorts to be shiny/strongly polite with respect to that set. Relying on these theoretical results, algorithms for crucial parts of these reductions are presented and their time complexities analysed. Besides providing alternative ways of proving that a theory satises the conditions of some of the Nelson-Oppen style combination theorems that have been proposed, these results allowed us to generalize a Nelson-Oppen style combination theorem. An application to graph colouring is presented.