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.^[1]

Definition

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.

Decidability

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

Solvers

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.

Applications

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]