约束 Horn 子句验证中的树维度

本文展示树维度的概念如何用于约束 Horn 子句（CHCs）的验证。树的维度是其分支复杂度的数值度量，此处概念适用于 Horn 子句推导树。维度为零的推导树对应于使用线性 CHCs 的推导，而更高维度的树源于使用非线性 CHCs 的推导。我们展示如何为 CHC 谓词增设一个表示维度的额外参数，使 CHC 验证器能推理推导维度的界。给定一组 CHCs $P$，我们定义 $P$ 的变换，产生维度有界的 CHCs 集合 $P^{\leq{k}}$。$P^{\leq{k}}$ 的推导由维度至多为 $k$ 的 $P$ 的推导组成。我们还展示如何构造记作 $P^{>{k}}$ 的子句集，其推导维度超过 $k$。随后我们给出利用这些构造分解 CHC 验证问题的算法。该分解的一种变体考虑维度依次递增的推导。本文包含实现描述与实验结果。稿件在 Theory and Practice of Logic Programming (TPLP) 审稿中。