This is a part of an ongoing research project, with the aim of finding the connections between properties related to theory combination in Satisfiability Modulo Theories. In previous work, 7 properties were analyzed: convexity, stable infiniteness, smoothness, finite witnessability, strong finite witnessability, the finite model property, and stable finiteness. The first two properties are related to Nelson-Oppen combination, the third and fourth to polite combination, the fifth to strong politeness, and the last two to shininess. However, the remaining key property of shiny theories, namely, the ability to compute the cardinalities of minimal models, was not yet analyzed. In this paper we study this property and its connection to the others.
翻译:本研究属于一项持续进行的研究项目,旨在寻找可满足性模理论中与理论组合相关的性质之间的联系。此前的研究已分析了7种性质:凸性、稳定无穷性、光滑性、有限可证性、强有限可证性、有限模型性质以及稳定有穷性。前两种性质与Nelson-Oppen组合相关,第三、四种与礼貌组合相关,第五种与强礼貌性相关,最后两种与闪亮性相关。然而,闪亮理论中另一关键性质——即计算极小模型基数的能力——尚未被分析。本文研究了该性质及其与其他性质之间的关联。