Tags:Satisfiability Modulo Theories, Theory Combination and Theory Politeness
Abstract:
We make two contributions to the study of theory combination in satisfiability modulo theories. The first is a table of examples for the Boolean combinations of the most common model-theoretic properties in theory combination, namely stable-infiniteness, smoothness, convexity, finite witnessability and strong finite witnessability (and therefore politeness and strong politeness as well); all of our examples are sharp, in the sense that we also offer proofs that no theories are available within simpler signatures. This table profoundly progresses the current understanding of the various properties and their interactions. The most remarkable example in this table is of a theory that is polite but not strongly polite, over a single sort (the existence of such a theory was only known until now for two-sorted signatures). The second contribution is a new combination theorem, according to which polite theory combination can be done for theories that are stably-infinite and strongly finitely witnessable, thus showing that smoothness is not a critical property in this combination method. This result has the potential of greatly simplifying proofs that show that a certain theory can be combined with any other theory using polite combination, as proving stable-infiniteness is much simpler than proving smoothness.
Combining Combination Properties: an Analysis of Stable-Infiniteness, Convexity, and Politeness