【AIMAメモ】推論規則(推論パターン)

命題論理のお話。

統語論を決める。
意味論にて、モデルの考え方を決める。ここでは、命題記号に直接真偽を割り当てるのがモデルとし、結合子の意味論は真理値表にて定義することにし、定義する。

すると、伴意の考え、および論理的同値の考えから、命題論理の複合文についての論理的同値関係がいろいろでてくる。ドモルガンの法則と呼ばれるものだとか、なんやかんや。

ここまでは命題論理の定義(= 統語論 + 意味論)からストレートな感じである。

で、推論規則(推論パターン)。

ここ、AIMAではヒューリスティックな流れだ。モーダスポーネンスとかAnd除去とかをどうやって導出するのか、もしくは何を推論規則と認定するかは曖昧である。例えば、And除去は論理的同値だが、モーダスポーネンスは違う。

ただ、何を推論規則とするかには何か法則性があるんだろうな、と感じる。

推論規則は証明に使えてナンボだと思うので、おそらくその観点での判断になるのかな。

また、推論規則を定めるまでは統語論と意味論が混ざっているが、推論規則を定めると、それは文の変形(書換え)のみになり、統語論だけで処理が進む。

伴意による推論アルゴリズムはモデルチェックであり、意味論ごりごりなわけだが、推論規則による証明という推論アルゴリズムは、統語論ごりごりであるという対比があるように思う。