Skip to Main content Skip to Navigation
Conference papers

Politeness for the Theory of Algebraic Datatypes (Extended Abstract)

Ying Sheng 1 Yoni Zohar 1 Christophe Ringeissen 2 Jane Lange 1 Pascal Fontaine 3, 4, 5 Clark Barrett 1 
2 PESTO - Proof techniques for security protocols
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
3 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
5 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
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.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-03346697
Contributor : Christophe Ringeissen Connect in order to contact the contributor
Submitted on : Thursday, September 16, 2021 - 3:19:45 PM
Last modification on : Friday, February 4, 2022 - 2:17:49 PM

Links full text

Identifiers

Collections

Citation

Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, et al.. Politeness for the Theory of Algebraic Datatypes (Extended Abstract). IJCAI 2021 - International Joint Conference on Artificial Intelligence (Sister Conferences Best Papers), Aug 2021, Montreal, Canada. pp.4829-4833, ⟨10.24963/ijcai.2021/660⟩. ⟨hal-03346697⟩

Share

Metrics

Record views

22