针对 Horn 子句可满足性的引理生成：一项初步研究

众所周知，命令式、函数式和逻辑式程序的验证可归约为受限 Horn 子句（CHC）的可满足性，且该可满足性检查可使用 CHC 求解器（如 Eldarica 和 Z3）来完成。这些求解器在作用于简单约束理论（如线性整数算术和布尔理论）时表现良好，但当子句涉及归纳定义结构（如列表或树）上的约束时，其效能大幅下降。近来，我们提出了一种消除这些归纳定义数据结构的变换技术，从而避免了在 CHC 求解器中引入归纳原理的需要。然而，当变换需要使用需巧妙生成的引理时，该技术可能失败。本文通过一个例子展示，在消除归纳定义结构的 CHC 变换过程中，如何引入称为差谓词的合适谓词，其定义对应于待引入的引理。通过第二个例子，我们展示当无法引入差谓词时，可转而引入同样对应于引理的辅助查询，且这些引理的证明可通过证明这些查询的可满足性来完成。