代数数据类型上约束 Horn 子句的可满足性：一种基于变换的方法
编程语言
2021-11-24 v1 计算机科学中的逻辑
摘要
我们解决定义在代数数据类型（ADTs，如列表与树）上的约束Horn子句（CHCs）的可满足性检查问题。我们提出了一种将定义在ADTs上的CHCs变换为谓词参数仅含基本类型（如整数与布尔量）的CHCs的新技术。因此，我们的技术在可满足性检查过程中避免显式使用基于ADTs归纳的证明规则。相较于以往ADT去除技术的主要扩展是一种称为差分替换的新变换规则，其允许我们引入辅助谓词，其定义对应于归纳证明中所用的引理。我们给出了一种通过应用新规则与传统折叠/展开规则来自动去除ADTs的算法。我们证明，在适当假设下，变换后子句集可满足当且仅当原子句集可满足。通过实验评估，我们表明新规则的使用显著提升了ADT去除的有效性。我们还表明，我们的方法相对于那些将归纳规则扩展至CHC求解器的工具具有竞争力。
引用
@article{arxiv.2111.11819,
title = {Satisfiability of Constrained Horn Clauses on Algebraic Data Types: A Transformation-based Approach},
author = {Emanuele De Angelis and Fabio Fioravanti and Alberto Pettorossi and Maurizio Proietti},
journal= {arXiv preprint arXiv:2111.11819},
year = {2021}
}
备注
This work has been SUBMITTED (under consideration) to the CILC 2020 specialissue of the Journal of Logic and Computation. arXiv admin note: text overlap with arXiv:2004.07749