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 verification and synthesis. Constrained Horn clauses can be seen as a form of constraint logic programming.{{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 }}
Definition
A constrained Horn clause is a formula of the form
\phi\land P_1(\mathbf{x}_1)\land \ldots\land P_n(\mathbf{x_n})\to P(\mathbf{x})
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.
Decidability
The satisfiability of constrained Horn clauses with constraints from linear integer arithmetic is undecidable.{{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}}
Solvers
There are several automated solvers for CHCs,{{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}} including the SPACER engine of Z3.{{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}}
CHC-COMP is an annual competition of CHC solvers.{{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}} CHC-COMP has run every year since 2018.
Applications
Constrained Horn clauses are a convenient language in which to specify problems in program verification.{{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}} The SeaHorn verifier for LLVM represents verification conditions as constrained Horn clauses,{{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}} as does the JayHorn verifier for Java.{{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}}
References
{{reflist}}