We address the problem of checking the satisfiability of a set of constrained Horn clauses (CHCs) possibly including more than one query. We propose a transformation technique that takes as input a set of CHCs, including a set of queries, and returns as output a new set of CHCs, such that the transformed CHCs are satisfiable if and only if so are the original ones, and the transformed CHCs incorporate in each new query suitable information coming from the other ones so that the CHC satisfiability algorithm is able to exploit the relationships among all queries. We show that our proposed technique is effective on a non trivial benchmark of sets of CHCs that encode many verification problems for programs manipulating algebraic data types such as lists and trees.

翻译：我们解决了检查一套限制的“角”条款(CHCs)的可比较性问题,其中可能包括一个以上的查询。我们建议采用一种转换技术,将一组“角”条款(包括一组查询)作为输入输入,并将返回作为输出,将一组新的“角”条款作为输出,这样,如果而且只有原始的“角”条款(CHCs)才具有可比较性,而且只有原始的“角”条款才具有可比较性,而转型的“角”条款在每个新的查询中都包含来自其它条款的合适信息,从而使“角”条款的可计算法能够利用所有查询之间的关系。我们表明,我们所提议的技术在一套“角”标准上是有效的,该标准将许多核查问题归为操纵代数数据类型的程序,如清单和树。