Politeness for the Theory of Algebraic Datatypes (Extended Abstract)

Sheng, Ying; Zohar, Yoni; Ringeissen, Christophe; Lange, Jane; Fontaine, Pascal; Barrett, Clark

doi:10.24963/ijcai.2021/660

Politeness for the Theory of Algebraic Datatypes (Extended Abstract)

Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark Barrett

Download BibTeX Cite

Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence. Sister Conferences Best Papers. Pages 4829-4833.

https://doi.org/10.24963/ijcai.2021/660

Keywords

Constraints and SAT: Constraint Satisfaction
Constraints and SAT: SAT: Algorithms and Techniques
Constraints and SAT: Satisfiability Modulo Theories
Constraints and SAT: Constraints: Modeling, Solvers, Applications

Abstract

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 also how it can be combined with other arbitrary disjoint theories using polite combination. Our results cover both inductive and finite datatypes, as well as their union. The combination method uses a new, simple, and natural notion of additivity, that enables deducing strong politeness from (weak) politeness.

Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, and Clark Barrett. 2021. Politeness for the Theory of Algebraic Datatypes (Extended Abstract). In Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI-21. IJCAI, 4829–4833. https://doi.org/10.24963/ijcai.2021/660

@inproceedings{ijcai2021p660,
  title     = {Politeness for the Theory of Algebraic Datatypes (Extended Abstract)},
  author    = {Sheng, Ying and Zohar, Yoni and Ringeissen, Christophe and Lange, Jane and Fontaine, Pascal and Barrett, Clark},
  booktitle = {Proceedings of the Thirtieth International Joint Conference on
               Artificial Intelligence, {IJCAI-21}},
  publisher = {International Joint Conferences on Artificial Intelligence Organization},
  editor    = {Prof. Zhi-Hua Zhou},
  pages     = {4829--4833},
  year      = {2021},
  month     = {8},
  note      = {Sister Conferences Best Papers},
  doi       = {10.24963/ijcai.2021/660},
  url       = {https://doi.org/10.24963/ijcai.2021/660},
}

TY  - CPAPER
TI  - Politeness for the Theory of Algebraic Datatypes (Extended Abstract)
AU  - Sheng, Ying
AU  - Zohar, Yoni
AU  - Ringeissen, Christophe
AU  - Lange, Jane
AU  - Fontaine, Pascal
AU  - Barrett, Clark
T2  - Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI-21
PB  - International Joint Conferences on Artificial Intelligence Organization
PY  - 2021
SP  - 4829
EP  - 4833
DO  - 10.24963/ijcai.2021/660
UR  - https://doi.org/10.24963/ijcai.2021/660
ER  -