关于代数数据类型:基于转变的办法的受限制的合角条款的可执行性 (Satisfiability of Constrained Horn Clauses on Algebraic Data Types: A Transformation-based Approach)

from arxiv, 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

We address the problem of checking the satisfiability of Constrained Horn Clauses (CHCs) defined on Algebraic Data Types (ADTs), such as lists and trees. We propose a new technique for transforming CHCs defined on ADTs into CHCs where the arguments of the predicates have only basic types, such as integers and booleans. Thus, our technique avoids, during satisfiability checking, the explicit use of proof rules based on induction over the ADTs. The main extension over previous techniques for ADT removal is a new transformation rule, called differential replacement, which allows us to introduce auxiliary predicates, whose definitions correspond to lemmas that are used when making inductive proofs. We present an algorithm that performs the automatic removal of ADTs by applying the new rule, together with the traditional folding/unfolding rules. We prove that, under suitable hypotheses, the set of the transformed clauses is satisfiable if and only if so is the set of the original clauses. By an experimental evaluation, we show that the use of the new rule significantly improves the effectiveness of ADT removal. We also show that our approach is competitive with respect to tools that extend CHC solvers with the use of inductive rules.

翻译：我们提出了一种新技术,将使用ADT的数据类型(ADTs)定义的CHC(ADTs)转换成CHCs。我们提出一种新的方法,将使用ADTs定义的HCs转换成CHCs,在这种情况下,上游参数只有基本类型,如整数和布林斯。因此,我们的技术避免了在对ADTs上岗时明确使用基于引导的证明规则。相对于先前的ADT删除技术而言,主要延伸是一个新的转换规则,称为差异替换,这使我们能够引入辅助性上游,其定义与诱导性证据中使用的 Lemmas相一致。我们提出了一种算法,通过应用新规则以及传统的折叠/折叠规则来自动清除ADTs。我们证明,在适当的假设下,经过修改的一套条款只有在原始条款组合在一起的情况下,才具有可置疑义性。我们通过实验性评估,表明新规则的使用大大改进了ADT规则的使用,从而大大改进了ADT规则的竞争性使用。我们还展示了ADT规则的使用。

相关内容