“Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness” by Guilherme V. Toledo, Yoni Zohar, and Clark Barrett. In Proceedings of the 29^th International Conference on Automated Deduction (CADE '23), (Brigitte Pientka and Cesare Tinelli, eds.), July 2023, pp. 522-541. Rome, Italy.
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.
BibTeX entry:
@inproceedings{TZB23-cade,
author = {Guilherme V. Toledo and Yoni Zohar and Clark Barrett},
editor = {Brigitte Pientka and Cesare Tinelli},
title = {Combining Combination Properties: An Analysis of Stable
Infiniteness, Convexity, and Politeness},
booktitle = {Proceedings of the {\it 29^{th}} International Conference
on Automated Deduction (CADE '23)},
series = {Lecture Notes in Artificial Intelligence},
volume = {14132},
pages = {522--541},
publisher = {Springer},
month = jul,
year = {2023},
doi = {10.1007/978-3-031-38499-8_30},
note = {Rome, Italy},
url = {https://link.springer.com/chapter/10.1007/978-3-031-38499-8_30}
}
(This webpage was created with bibtex2web.)