制約付きホーン節

制約ホーン節（CHC）は、プログラムの検証と合成に応用される一階述語論理の一部である。制約ホーン節は、制約論理プログラミングの一種とみなすことができる。^[1]

意味

制約付きホーン節は、次の形式の式である。

$\phi \land P_{1}(\mathbf {x} _{1})\land \ldots \land P_{n}(\mathbf {x_{n}} )\to P(\mathbf {x} )$

ここで、はある一階述語理論における制約であり、は述語であり、は普遍量化された変数です。制約の追加により、これは単純なホーン節の一般化になります。 $\phi$ $P_{i}$ $\mathbf {x} _{i}$

決定可能性

線形整数演算からの制約を伴う制約付きホーン節の充足可能性は決定不可能である。^[2]

ソルバー

CHC用の自動ソルバーはいくつかあり、^[3]Z3のSPACERエンジンもその1つである。^[4]

CHC-COMPはCHCソルバーの年次コンテストです。^[5] CHC-COMPは2018年から毎年開催されています。

アプリケーション

制約付きホーン節は、プログラム検証における問題を指定するのに便利な言語です。^[6]LLVMのSeaHorn検証器は、検証条件を制約付きホーン節として表現します。^[7]JavaのJayHorn検証器も同様です。^[8]

参考文献

^ Angelis, Emanuele De; Fioravanti, Fabio; Gallagher, John P.; Hermenegildo, Manuel V.; Pettorossi, Alberto; Proietti, Maurizio (2022年11月). 「プログラム検証のための制約付きホーン節の分析と変換」.論理プログラミングの理論と実践. 22 (6): 974– 1042. arXiv : 2108.00739 . doi : 10.1017/S1471068421000211 . ISSN 1471-0684. S2CID 236777105. CHCは、構文的にも意味的にも制約論理プログラムと同じです。
^ Cox, Jim; McAloon, Ken; Tretkoff, Carol (1992-06-01). 「計算複雑性と制約論理プログラミング言語」. Annals of Mathematics and Artificial Intelligence . 5 (2): 163– 189. doi :10.1007/BF01543475. ISSN 1573-7470. S2CID 666608.
^ Blicha, Martin; Britikov, Konstantin; Sharygina, Natasha (2023). 「The Golem Horn Solver」。Enea, Constantin; Lal, Akash (eds.) 著。コンピュータ支援検証。コンピュータサイエンスの講義ノート。Cham: Springer Nature Switzerland。pp. 209– 223。doi : 10.1007 /978-3-031-37703-7_10。ISBN 978-3-031-37703-7。
^ Gurfinkel, Arie (2022). 「制約付きホーン節によるプログラム検証（招待論文）」。Shoham, Sharon、Vizel, Yakir（編）「コンピュータ支援検証」。コンピュータサイエンスの講義ノート。第13371巻。Cham：Springer International Publishing。pp. 19– 29。doi ：10.1007 / 978-3-031-13185-1_2。ISBN 978-3-031-13185-1。
^ Fedyukovich, Grigory; Rümmer, Philipp (2021-09-10). 「コンペティションレポート: CHC-COMP-21」.理論計算機科学電子会議. 344 : 91–108 . arXiv : 2109.04635v1 . doi :10.4204/EPTCS.344.7. S2CID 221132231.
^ Bjørner, Nikolaj; Gurfinkel, Arie; McMillan, Ken; Rybalchenko, Andrey (2015), Beklemishev, Lev D.; Blass, Andreas; Dershowitz, Nachum; Finkbeiner, Bernd (eds.)、「プログラム検証のためのホーン節ソルバー」、Fields of Logic and Computation II: Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday、Lecture Notes in Computer Science、Cham: Springer International Publishing、pp. 24– 51、doi :10.1007/978-3-319-23534-9_2、ISBN 978-3-319-23534-9、 2023-12-07取得
^ Gurfinkel, Arie; Kahsai, Temesghen; Komuravelli, Anvesh; Navas, Jorge A. (2015). 「The SeaHorn Verification Framework」。Kroening, Daniel; Păsăreanu, Corina S. (eds.). Computer Aided Verification . Lecture Notes in Computer Science. Cham: Springer International Publishing. pp. 343– 361. doi :10.1007/978-3-319-21690-4_20. ISBN 978-3-319-21690-4。
^ カサイ、テメスゲン;ルマー、フィリップ。サンチェス、ワスカル。マーティン・シェーフ (2016)。「JayHorn: Java プログラムを検証するためのフレームワーク」。スワラット州チャウドゥリにて。ファーザン、アザデ（編）。コンピュータ支援による検証。コンピューターサイエンスの講義ノート。チャム：シュプリンガー・インターナショナル・パブリッシング。 pp. 352–358。土井:10.1007/978-3-319-41528-4_19。ISBN 978-3-319-41528-4。

[1] Angelis, Emanuele De; Fioravanti, Fabio; Gallagher, John P.; Hermenegildo, Manuel V.; Pettorossi, Alberto; Proietti, Maurizio (2022年11月). 「プログラム検証のための制約付きホーン節の分析と変換」.論理プログラミングの理論と実践. 22 (6): 974– 1042. arXiv : 2108.00739 . doi : 10.1017/S1471068421000211 . ISSN 1471-0684. S2CID 236777105. CHCは、構文的にも意味的にも制約論理プログラムと同じです。

[2] Cox, Jim; McAloon, Ken; Tretkoff, Carol (1992-06-01). 「計算複雑性と制約論理プログラミング言語」. Annals of Mathematics and Artificial Intelligence . 5 (2): 163– 189. doi :10.1007/BF01543475. ISSN 1573-7470. S2CID 666608.

[3] Blicha, Martin; Britikov, Konstantin; Sharygina, Natasha (2023). 「The Golem Horn Solver」。Enea, Constantin; Lal, Akash (eds.) 著。コンピュータ支援検証。コンピュータサイエンスの講義ノート。Cham: Springer Nature Switzerland。pp. 209– 223。doi : 10.1007 /978-3-031-37703-7_10。ISBN 978-3-031-37703-7。

[4] Gurfinkel, Arie (2022). 「制約付きホーン節によるプログラム検証（招待論文）」。Shoham, Sharon、Vizel, Yakir（編）「コンピュータ支援検証」。コンピュータサイエンスの講義ノート。第13371巻。Cham：Springer International Publishing。pp. 19– 29。doi ：10.1007 / 978-3-031-13185-1_2。ISBN 978-3-031-13185-1。

[5] Fedyukovich, Grigory; Rümmer, Philipp (2021-09-10). 「コンペティションレポート: CHC-COMP-21」.理論計算機科学電子会議. 344 : 91–108 . arXiv : 2109.04635v1 . doi :10.4204/EPTCS.344.7. S2CID 221132231.

[6] Bjørner, Nikolaj; Gurfinkel, Arie; McMillan, Ken; Rybalchenko, Andrey (2015), Beklemishev, Lev D.; Blass, Andreas; Dershowitz, Nachum; Finkbeiner, Bernd (eds.)、「プログラム検証のためのホーン節ソルバー」、Fields of Logic and Computation II: Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday、Lecture Notes in Computer Science、Cham: Springer International Publishing、pp. 24– 51、doi :10.1007/978-3-319-23534-9_2、ISBN 978-3-319-23534-9、 2023-12-07取得

[7] Gurfinkel, Arie; Kahsai, Temesghen; Komuravelli, Anvesh; Navas, Jorge A. (2015). 「The SeaHorn Verification Framework」。Kroening, Daniel; Păsăreanu, Corina S. (eds.). Computer Aided Verification . Lecture Notes in Computer Science. Cham: Springer International Publishing. pp. 343– 361. doi :10.1007/978-3-319-21690-4_20. ISBN 978-3-319-21690-4。

[8] カサイ、テメスゲン;ルマー、フィリップ。サンチェス、ワスカル。マーティン・シェーフ (2016)。「JayHorn: Java プログラムを検証するためのフレームワーク」。スワラット州チャウドゥリにて。ファーザン、アザデ（編）。コンピュータ支援による検証。コンピューターサイエンスの講義ノート。チャム：シュプリンガー・インターナショナル・パブリッシング。 pp. 352–358。土井:10.1007/978-3-319-41528-4_19。ISBN 978-3-319-41528-4。