Constrained Horn clauses

带有一阶理论约束的 Horn Clause，形如：

$$\phi \wedge P_1(x)\wedge P_2(x)\dots \to P(x)$$

其中 $P_1,P_2,\dots P$ 是未解释的谓词符号，$\phi$ 是背景一阶理论中的公式。$P(x)$ 处 (Head) 也可以是约束 $\psi$（不过等价地，可以把 $\psi$ 换到 body 部分，保证 head 只可能是未解释谓词项或者False）

CHC 中的变量隐式为全称量词所约束。

分类

1. Goal/Query Clause：Head 处为约束 $\psi$ （尤其是False）
2. Fact Clause: Head 处未解释谓词，body 为约束

判定

约束为 linear integer arithmetic 的 CHC 可满足性不可判定

CHC 求解器

• Z3/Spacer
• SeaHorn
• …