「ホーン節」の版間の差分
ナビゲーションに移動
検索に移動
細 ("ホーン節" を保護しました。 [edit=sysop:move=sysop]) |
|
(相違点なし)
| |
2007年7月20日 (金) 11:07時点における版
【ほーんせつ (Horn clause)】
リテラル(命題そのものか, またはその否定)が選言で結合された論理式を節と呼び, 正のリテラル(否定のついていない命題)を高々1つ含む節のことをホーン節と呼ぶ. Prolog などの多くの論理型プログラムはホーン節の集合として構成される. 任意の論理式は等価な節集合に変換できるが, 特にホーン節のみからなる節集合に対しての定理証明手続きは, 線形導出などの効率的な手続きが存在することが知られている.