View source for Constrained Horn clauses

{{Short description|Fragment of first-order logic}}
{{Missing information|date=December 2023|if they are named after somebody? When were they first defined? Perhaps add an example?}}
'''Constrained Horn clauses''' (CHCs) are a fragment of [[first-order logic]] with applications to program [[Formal verification|verification]] and [[Program synthesis|synthesis]]. Constrained Horn clauses can be seen as a form of [[constraint logic programming]].<ref>{{Cite journal |last1=Angelis |first1=Emanuele De |last2=Fioravanti |first2=Fabio |last3=Gallagher |first3=John P. |last4=Hermenegildo |first4=Manuel V. |last5=Pettorossi |first5=Alberto |last6=Proietti |first6=Maurizio |date=November 2022 |title=Analysis and Transformation of Constrained Horn Clauses for Program Verification |journal=Theory and Practice of Logic Programming |language=en |volume=22 |issue=6 |pages=974–1042 |doi=10.1017/S1471068421000211 |s2cid=236777105 |issn=1471-0684|quote=CHCs are syntactically and semantically the same as constraint logic programs|doi-access=free |arxiv=2108.00739 }}</ref>

== Definition ==

A constrained Horn clause is a [[Well-formed formula|formula]] of the form

<math>
  \phi\land P_1(\mathbf{x}_1)\land \ldots\land P_n(\mathbf{x_n})\to P(\mathbf{x})
</math>

where <math>\phi</math> is a ''constraint'' in some first-order theory, <math>P_i</math> are predicates, and <math>\mathbf{x}_i</math> 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 problem|undecidable]].<ref>{{Cite journal |last1=Cox |first1=Jim |last2=McAloon |first2=Ken |last3=Tretkoff |first3=Carol |date=1992-06-01 |title=Computational complexity and constraint logic programming languages |url=https://doi.org/10.1007/BF01543475 |journal=Annals of Mathematics and Artificial Intelligence |language=en |volume=5 |issue=2 |pages=163–189 |doi=10.1007/BF01543475 |s2cid=666608 |issn=1573-7470}}</ref>

== Solvers ==

There are several automated solvers for CHCs,<ref>{{Cite book |last1=Blicha |first1=Martin |last2=Britikov |first2=Konstantin |last3=Sharygina |first3=Natasha |date=2023 |editor-last=Enea |editor-first=Constantin |editor2-last=Lal |editor2-first=Akash |chapter=The Golem Horn Solver |chapter-url=https://link.springer.com/chapter/10.1007/978-3-031-37703-7_10 |title=Computer Aided Verification |series=Lecture Notes in Computer Science |language=en |location=Cham |publisher=Springer Nature Switzerland |pages=209–223 |doi=10.1007/978-3-031-37703-7_10 |isbn=978-3-031-37703-7}}</ref> including the SPACER engine of [[Z3 Theorem Prover|Z3]].<ref>{{Cite book |last=Gurfinkel |first=Arie |date=2022 |editor-last=Shoham |editor-first=Sharon |editor2-last=Vizel |editor2-first=Yakir |chapter=Program Verification with Constrained Horn Clauses (Invited Paper) |chapter-url=https://link.springer.com/chapter/10.1007/978-3-031-13185-1_2 |title=Computer Aided Verification |series=Lecture Notes in Computer Science |volume=13371 |language=en |location=Cham |publisher=Springer International Publishing |pages=19–29 |doi=10.1007/978-3-031-13185-1_2 |isbn=978-3-031-13185-1}}</ref>

CHC-COMP is an annual competition of CHC solvers.<ref>{{Cite journal |last1=Fedyukovich |first1=Grigory |last2=Rümmer |first2=Philipp |date=2021-09-10 |title=Competition Report: CHC-COMP-21 |journal=Electronic Proceedings in Theoretical Computer Science |volume=344 |pages=91–108 |doi=10.4204/EPTCS.344.7 |arxiv=2109.04635v1 |s2cid=221132231 |language=en}}</ref> CHC-COMP has run every year since 2018.

== Applications ==

Constrained Horn clauses are a convenient language in which to specify problems in program verification.<ref>{{Citation |last1=Bjørner |first1=Nikolaj |title=Horn Clause Solvers for Program Verification |date=2015 |url=https://doi.org/10.1007/978-3-319-23534-9_2 |work=Fields of Logic and Computation II: Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday |pages=24–51 |editor-last=Beklemishev |editor-first=Lev D. |access-date=2023-12-07 |series=Lecture Notes in Computer Science |place=Cham |publisher=Springer International Publishing |language=en |doi=10.1007/978-3-319-23534-9_2 |isbn=978-3-319-23534-9 |last2=Gurfinkel |first2=Arie |last3=McMillan |first3=Ken |last4=Rybalchenko |first4=Andrey |editor2-last=Blass |editor2-first=Andreas |editor3-last=Dershowitz |editor3-first=Nachum |editor4-last=Finkbeiner |editor4-first=Bernd}}</ref> The SeaHorn verifier for [[LLVM]] represents verification conditions as constrained Horn clauses,<ref>{{Cite book |last1=Gurfinkel |first1=Arie |last2=Kahsai |first2=Temesghen |last3=Komuravelli |first3=Anvesh |last4=Navas |first4=Jorge A. |date=2015 |editor-last=Kroening |editor-first=Daniel |editor2-last=Păsăreanu |editor2-first=Corina S.|editor2-link= Corina Păsăreanu |chapter=The SeaHorn Verification Framework |chapter-url=https://link.springer.com/chapter/10.1007/978-3-319-21690-4_20 |title=Computer Aided Verification |series=Lecture Notes in Computer Science |language=en |location=Cham |publisher=Springer International Publishing |pages=343–361 |doi=10.1007/978-3-319-21690-4_20 |isbn=978-3-319-21690-4}}</ref> as does the JayHorn verifier for [[Java (programming language)|Java]].<ref>{{Cite book |last1=Kahsai |first1=Temesghen |last2=Rümmer |first2=Philipp |last3=Sanchez |first3=Huascar |last4=Schäf |first4=Martin |date=2016 |editor-last=Chaudhuri |editor-first=Swarat |editor2-last=Farzan |editor2-first=Azadeh |chapter=JayHorn: A Framework for Verifying Java programs |chapter-url=https://link.springer.com/chapter/10.1007/978-3-319-41528-4_19 |title=Computer Aided Verification |series=Lecture Notes in Computer Science |language=en |location=Cham |publisher=Springer International Publishing |pages=352–358 |doi=10.1007/978-3-319-41528-4_19 |isbn=978-3-319-41528-4}}</ref>

== References ==
{{reflist}}

[[Category:Formal logic]]