Politeness for the Theory of Algebraic Datatypes

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...

Descripción completa

Detalles Bibliográficos
Autores principales: Sheng, Ying, Zohar, Yoni, Ringeissen, Christophe, Lange, Jane, Fontaine, Pascal, Barrett, Clark
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324139/
http://dx.doi.org/10.1007/978-3-030-51074-9_14
_version_ 1783551888831021056
author Sheng, Ying
Zohar, Yoni
Ringeissen, Christophe
Lange, Jane
Fontaine, Pascal
Barrett, Clark
author_facet Sheng, Ying
Zohar, Yoni
Ringeissen, Christophe
Lange, Jane
Fontaine, Pascal
Barrett, Clark
author_sort Sheng, Ying
collection PubMed
description 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.
format Online
Article
Text
id pubmed-7324139
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73241392020-06-30 Politeness for the Theory of Algebraic Datatypes Sheng, Ying Zohar, Yoni Ringeissen, Christophe Lange, Jane Fontaine, Pascal Barrett, Clark Automated Reasoning Article 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. 2020-05-30 /pmc/articles/PMC7324139/ http://dx.doi.org/10.1007/978-3-030-51074-9_14 Text en © Springer Nature Switzerland AG 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic.
spellingShingle Article
Sheng, Ying
Zohar, Yoni
Ringeissen, Christophe
Lange, Jane
Fontaine, Pascal
Barrett, Clark
Politeness for the Theory of Algebraic Datatypes
title Politeness for the Theory of Algebraic Datatypes
title_full Politeness for the Theory of Algebraic Datatypes
title_fullStr Politeness for the Theory of Algebraic Datatypes
title_full_unstemmed Politeness for the Theory of Algebraic Datatypes
title_short Politeness for the Theory of Algebraic Datatypes
title_sort politeness for the theory of algebraic datatypes
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324139/
http://dx.doi.org/10.1007/978-3-030-51074-9_14
work_keys_str_mv AT shengying politenessforthetheoryofalgebraicdatatypes
AT zoharyoni politenessforthetheoryofalgebraicdatatypes
AT ringeissenchristophe politenessforthetheoryofalgebraicdatatypes
AT langejane politenessforthetheoryofalgebraicdatatypes
AT fontainepascal politenessforthetheoryofalgebraicdatatypes
AT barrettclark politenessforthetheoryofalgebraicdatatypes

Ejemplares similares