arXiv Open Access 2020

Politeness for the Theory of Algebraic Datatypes

Ying Sheng Yoni Zohar Christophe Ringeissen Jane Lange Pascal Fontaine +1 lainnya

Lihat Sumber

Abstrak

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.

Topik & Kata Kunci

cs.LO

Penulis (6)

Ying Sheng

Yoni Zohar

Christophe Ringeissen

Jane Lange

Pascal Fontaine

Clark Barrett

Format Sitasi

APA MLA BibTeX

Sheng, Y., Zohar, Y., Ringeissen, C., Lange, J., Fontaine, P., Barrett, C. (2020). Politeness for the Theory of Algebraic Datatypes. https://arxiv.org/abs/2004.04854

Akses Cepat

Lihat di Sumber

Informasi Jurnal

Tahun Terbit: 2020
Bahasa: en
Sumber Database: arXiv
Akses: Open Access ✓