【AIMAメモ】融合規則からホーン節へ

で、融合規則(resolution rule)なる推論規則が注目される。これは、命題論理においては、この推論規則たったひとつで完全である。すなわち、KBから伴意される任意の文を導出できる。モーダスポーネンスもなんもかんもいらないのだ。

ここで、命題論理における任意の文がk-CNFの形で書けることが重要な役割をもっていることになる。するとKBも、任意の文αもk-CNFだから、融合法を適用できる。

この文脈でホーン節、登場。

融合法(= 融合規則+探索)は強力だが、そのままで使うのではなく、文に含まれる節の形を多少制限するといろいろメリットがある。それがホーン節。

ホーン節は正リテラルを高々ひとつ含む選言節である。

(¬A∨¬B∨C)はホーン節だが、(¬A∨B∨C)はホーン節ではない。ホーン節は含意に変形できる。例えば、

(¬A∨¬B∨C) は (A∧B)⇒C、

とか。ここで(A∧B)の部分を体部(body)と呼び、Cの部分を頭部(head)と呼ぶ。

ここでPrologと繼がった！　Prologの記法だと、

C := A,B.

であり、左右が逆だが意味は同じ。

head := body.

なので用語も同じ。

ただしここでの話は命題論理なので、FOLとの関係はどうなっているのというのはわからない。まだ関連が見えただけ。