Constrained Horn Clauses (CHCs) are often used in automated program verification. Thus, techniques for (dis-)proving satisfiability of CHCs are a very active field of research. On the other hand, acceleration techniques for computing formulas that characterize the N-fold closure of loops have successfully been used for static program analysis. We show how to use acceleration to avoid repeated derivations with recursive CHCs in resolution proofs, which reduces the length of the proofs drastically. This idea gives rise to a novel calculus for (dis)proving satisfiability of CHCs, called Acceleration Driven Clause Learning (ADCL). We implemented this new calculus in our tool LoAT and evaluate it empirically in comparison to other state-of-the-art tools.

翻译：约束霍恩子句（Constrained Horn Clauses, CHCs）常用于自动化程序验证。因此，证明或证伪CHC可满足性的技术是一个非常活跃的研究领域。另一方面，用于计算表征循环N次闭包公式的加速技术已成功应用于静态程序分析。我们展示了如何利用加速来避免在归结证明中重复推导递归CHC，这极大地缩短了证明长度。这一思想催生了一种新的用于证明或证伪CHC可满足性的演算方法，称为加速驱动子句学习（Acceleration Driven Clause Learning, ADCL）。我们在工具LoAT中实现了这一新演算，并与其他现有工具进行了实证评估比较。