“Polite Combination of Algebraic Datatypes” by Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, and Clark Barrett. Journal of Automated Reasoning, vol. 66, no. 3, Aug. 2022, pp. 331-335, Springer.
Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). Since its latest stable version, the SMT-LIB standard defines a theory of algebraic datatypes, which is currently supported by several mainstream SMT solvers. In this paper, we study this particular theory of datatypes and prove that it is strongly polite, showing how it can be combined with other arbitrary disjoint theories using polite combination. The combination method uses a new, simple, and natural notion of additivity that enables deducing strong politeness from (weak) politeness.
Keywords: Satisfiability Modulo Theories, Automated reasoning, Theory combination, Algebraic datatypes, Polite combination
BibTeX entry:
@article{SZR+22,
author = {Ying Sheng and Yoni Zohar and Christophe Ringeissen and Jane
Lange and Pascal Fontaine and Clark Barrett},
title = {Polite Combination of Algebraic Datatypes},
journal = {Journal of Automated Reasoning},
volume = {66},
number = {3},
pages = {331--335},
publisher = {Springer},
month = aug,
year = {2022},
doi = {10.1007/s10817-022-09625-3},
url = {https://rdcu.be/cMVOR}
}
(This webpage was created with bibtex2web.)