Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness

TL;DR

This paper provides a comprehensive table of examples for key model-theoretic properties in theory combination and introduces a new theorem simplifying the conditions needed for polite theory combination, advancing the understanding of SMT theory interactions.

Contribution

It offers a detailed table of sharp examples for properties like stable infiniteness and convexity, and presents a new combination theorem reducing the requirements for polite theory combination.

Findings

A theory over a single sort can be polite but not strongly polite.

Smoothness is not necessary for polite theory combination if other conditions are met.

Stable infiniteness and strong finite witnessability suffice for polite combination.

Abstract

We make two contributions to the study of theory combination in satisfiability modulo theories. The first is a table of examples for the 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 significantly progresses the current understanding of the various properties and their interactions. The most remarkable example in this table is of a theory over a single sort that is polite but not strongly polite (the existence of such a theory was only known until now for two-sorted signatures). The second contribution is a new combination theorem showing that in order to apply polite theory combination, it is sufficient for one theory to be stably infinite and strongly finitely witnessable, thus showing that smoothness is not a critical property in this combination method. This result has the potential to greatly simplify the process of showing which theories can be used in polite combination, as showing stable infiniteness is considerably simpler than showing smoothness.