Authors: Dejan Jovanovic and Clark Barrett


Title: Polite Theories Revisited

 Abstract: 
 The classic method of Nelson and Oppen for combining decision procedures 
 requires the theories to be stably-infnite. Unfortunately, some 
 important theories do not fall into this category (e.g. the theory of 
 bit-vectors). To remedy this problem, previous work introduced the 
 notion of polite theories. Polite theories can be combined with any 
 other theory using an extension of the Nelson-Oppen approach. In this 
 paper we revisit the notion of polite theories, fxing a subtle flaw in 
 the original definition. We give a new combination theorem which 
 specifies the degree to which politeness is preserved when combining 
 polite theories. We also give conditions under which politeness is 
 preserved when instantiating theories by identifying two sorts. These 
 results lead to a more general variant of the theorem for combining 
 multiple polite theories.