Polite Combination of Algebraic Datatypes
Polite Combination of Algebraic Datatypes
复制标题
代数数据类型的礼貌组合
DOI：
--
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Clark W. Barrett
中科院分区：
文献类型：
--
作者：
Ying Sheng;Yoni Zohar;C. Ringeissen;Jane Lange;P. Fontaine;Clark W. Barrett
代数数据类型，其中包括列表和树，已经引起了人们对自动推理和可满足模理论（SMT）的极大兴趣。自其最新稳定版本以来，SMT- lib标准定义了代数数据类型理论，目前由几个主流SMT求解器支持。在本文中，我们研究了这种特殊的数据类型理论，并证明了它是强礼貌的，展示了它如何使用礼貌组合与其他任意不相交的理论相结合。组合方法使用了一种新的、简单的、自然的可加性概念，可以从（弱）礼貌中推断出强礼貌。
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.
DOI：
10.1007/978-3-642-28756-5_47
发表时间：
2012
期刊：
--
影响因子：
--
作者：
Basler G
通讯作者：
Basler G