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]
A constrained Horn clause is a formula of the form
where is a constraint in some first-order theory, are predicates, and are universally-quantified variables.
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]