树与代数（Co）数据树的扩展理论
The Extended Theory of Trees and Algebraic (Co)datatypes
摘要：
有限树和无限树的一阶理论自80年代以来一直在研究，特别是在逻辑编程社区。继Dadoul，道和Frühouth，我们考虑这个理论的扩展与一个额外的谓词有限的树，这是有用的表达属性（不仅databases，但也）codatabases。基于他们的工作，我们提出了一个简化过程，确定是否任何给定的（不一定封闭）公式是可满足的，返回一个简化的公式，使人们能够读出所有可能的模型。我们的扩展使算法可用于代数（共）datestries，这是不可能的，在他们原来的工作，由于限制性的假设。我们还提供了一个原型实现我们的简化过程，并从SMT-LIB的实例进行评估。
英文摘要：
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ühwirth, 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
