标题： 组合性质的结合：稳定无限性、凸性和礼貌性的分析 显示英文标题

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

摘要： 我们对满足理论组合的研究做出了两项贡献。 第一项是关于理论组合中最常见的模型论性质的组合示例表，即稳定无限性、平滑性、凸性、有限可证性和强有限可证性（因此也包括礼貌性和强礼貌性）。 我们的所有示例都是精确的，也就是说，我们还提供了证明，表明在更简单的符号中没有可用的理论。 该表显著推进了当前对各种性质及其相互作用的理解。 该表中最引人注目的例子是一个单排序理论，它是礼貌的但不是强礼貌的（直到现在，这种理论仅在双排序符号中已知存在）。 第二项贡献是一个新的组合定理，表明为了应用礼貌理论组合，只需一个理论是稳定无限且强有限可证的，从而表明平滑性在这个组合方法中并不是一个关键性质。 这一结果有可能大大简化展示哪些理论可以用于礼貌组合的过程，因为证明稳定无限性比证明平滑性要简单得多。 显示英文摘要

摘要： 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.