Constrained Horn clauses

A constrained Horn clause is a formula of the form

${\displaystyle \phi \land P_{1}(\mathbf {x} _{1})\land \ldots \land P_{n}(\mathbf {x_{n}} )\to P(\mathbf {x} )}$

where ${\displaystyle \phi }$ is a constraint in some first-order theory, ${\displaystyle P_{i}}$ are predicates, and ${\displaystyle \mathbf {x} _{i}}$ are universally-quantified variables. The addition of constraint makes it a generalization of the plain Horn clause.

The satisfiability of constrained Horn clauses with constraints from linear integer arithmetic is undecidable.^[2]

There are several automated solvers for CHCs,^[3] including the SPACER engine of Z3.^[4]

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

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