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$

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

分类

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

判定

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

CHC 求解器

• Z3/Spacer
• SeaHorn
• …