AIConfPaper
IJCAI 2021poster0 citations

Politeness for the Theory of Algebraic Datatypes (Extended Abstract)

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

Source ↗PDF ↗

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.

Constraints and SAT: Satisfiability Modulo TheoriesConstraints and SAT: SAT: Algorithms and TechniquesConstraints and SAT: Constraints: Modeling, Solvers, ApplicationsConstraints and SAT: Constraint Satisfaction
BibTeX
@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    = {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},
}
Politeness for the Theory of Algebraic Datatypes (Extended Abstract) · IJCAI 2021