制約付きホーン節

制約付きホーン節（CHC）は、プログラム検証や合成に応用される一階述語論理の断片をモデル化したものです。これは、論理学者アルフレッド・ホーンにちなんで名付けられた一般的なホーン節にちなんで名付けられています。特に制約付きホーン節は、制約論理プログラミングの一形態と見なすことができます。^{[ 1 ]}

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

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

どこ${\displaystyle \phi }$ある一次理論における制約であり、${\displaystyle P_{i}}$述語であり、${\displaystyle \mathbf {x} _{i}}$これらは全称量化変数です。制約を追加することで、通常のホーン節の一般化となります。

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

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

CHC-COMPはCHCソルバーの年次競技会です。^{[ 5 ]} CHC-COMPは2018年から毎年開催されています。

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