Constrained Horn Clauses

Constrained Horn clauses (CHCs) are a fragment of first-order logic with applications to program verification and synthesis. Constrained Horn clauses can be seen as a form of constraint logic programming.

Definition

A constrained Horn clause is a formula of the form

$\phi\land P_1(\mathbf_1)\land \ldots\land P_n(\mathbf)\to P(\mathbf)$

where $\phi$ is a ''constraint'' in some first-order theory, $P_i$ are predicates, and $\mathbf_i$ are universally-quantified variables. The addition of constraint makes it a generalization of the plain Horn clause.

Decidability

The satisfiability of constrained Horn clauses with constraints from linear integer arithmetic is undecidable.

Solvers

There are several automated solvers for CHCs, including the SPACER engine of Z3.

CHC-COMP is an annual competition of CHC solvers. CHC-COMP has run every year since 2018.

Applications

Constrained Horn clauses are a convenient language in which to specify problems in program verification. The SeaHorn verifier for LLVM represents verification conditions as constrained Horn clauses, as does the JayHorn verifier for Java.

References

{{reflist

Formal logic