The Extended Theory of Trees and Algebraic (Co)datatypes

Autor:	Zaiser, Fabian, Ong, C. -H. Luke
Rok vydání:	2020
Předmět:	Computer Science - Logic in Computer Science Computer Science - Symbolic Computation
Zdroj:	EPTCS 320, 2020, pp. 167-196
Druh dokumentu:	Working Paper
DOI:	10.4204/EPTCS.320.14
Popis:	The first-order theory of finite and infinite trees has been studied since the eighties, especially by the logic programming community. Following Djelloul, Dao and Fr\"uhwirth, we consider an extension of this theory with an additional predicate for finiteness of trees, which is useful for expressing properties about (not just datatypes but also) codatatypes. Based on their work, we present a simplification procedure that determines whether any given (not necessarily closed) formula is satisfiable, returning a simplified formula which enables one to read off all possible models. Our extension makes the algorithm usable for algebraic (co)datatypes, which was impossible in their original work due to restrictive assumptions. We also provide a prototype implementation of our simplification procedure and evaluate it on instances from the SMT-LIB. Comment: In Proceedings VPT/HCVS 2020, arXiv:2008.02483
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2005.06659 Zobrazit plný text záznamu View this record from Arxiv