Top Qs
Timeline
Chat
Perspective
Constrained Horn clauses
Fragment of first-order logic From Wikipedia, the free encyclopedia
Remove ads
Constrained Horn clauses (CHCs) model a fragment of first-order logic with applications to program verification and synthesis. They are named after the general Horn clause, which in turn is named after logician Alfred Horn. Constrained Horn clauses, specifically, can be seen as a form of constraint logic programming.[1]
This article is missing information about when these clauses were first defined. Perhaps add an example. (December 2023) |
Remove ads
Definition
Summarize
Perspective
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 addition of constraint makes it a generalization of the plain Horn clause.
Remove ads
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]
References
Wikiwand - on
Seamless Wikipedia browsing. On steroids.
Remove ads