一次論理 (FOL) 文を接続正規形 (CNF) に変換し、解決を実行することに関するいくつかのメモを読んでいます。
CNF に変換する手順の 1 つは、 ですStandardize variables。
変数を標準化しない場合、解決アルゴリズムの完全な条件が違反し、健全性が違反しない理由を見つけるために検索してきました。
完全性に違反し、健全性が維持される理由を誰でも追加できますか?
1 に答える
1
これを視覚化するのに役立つ例を次に示します。あなたの理論が
(for all X : nice(X)) or (for all X : smart(X)) (1)
これを別々に標準化すると、CNF になります。
nice(X) or smart(Y)
つまり、人口の全員が親切であるか、人口の全員が頭が良いか、またはその両方です。
標準化をバラバラにドロップすると、CNFが生成されます
nice(X) or smart(X)
これはと同等です
(for all X : nice(X) or smart(X)) (2)
つまり、母集団内の各個人について、その個人はいい人、賢い人、またはその両方です。
この理論 (2) は、元の理論 (1) よりも弱いと言っています。なぜなら、それは、誰もが親切であるということは真実ではないという状況を認めているからです。各個人がどちらか一方、または両方であることは事実です。言い換えると、(2) は (1) を意味するのではなく、(1) は (2) を意味します (集団全体がナイスであれば、各個人はナイスです。集団全体がスマートであれば、各個人はスマートです。したがって、 、各個人はいい人か賢い人です）。(2) で受け入れられる可能世界の集合は、(1) で受け入れられる可能世界の集合より厳密に大きい。
これは、完全性と健全性について何と言っていますか?
(2) の使用は完全ではありません。これは、(2) を使用すると真であると証明されない (1) の真の定理の反例を示すことができるためです。「ジョンがナイスではなく頭がいいなら、リズは頭がいい」という定理を考えてみましょう。(1) を考えると、これは真です。人口全体がこれら 2 つの資質のいずれかを共有している場合、ジョンは親切ではないので「賢い」に違いないため、リズ (および他のすべての人) もスマートでなければならないからです。ただし、(2) を考えると、これはもはや真実ではありません (リズはいい人ですが賢くはなく、他の人はどちらか一方である可能性がありますが、(2) を考えるとまだ問題ありません)。したがって、(2) を使用して真の定理を証明することはできなくなり(標準化をバラバラにした後)、したがって、私の推論は完全ではありません。
ここで、(2) を使用して、ある定理 T が真であることを証明するとします。これは、(2) が成立するすべての可能な世界で T が成立することを意味します。これには、(1) で成立するもののサブセットも含まれます (ここから上の 3 番目の段落によると)。したがって、T は (1) でも真であるため、(2) を使用して推論を実行することは依然として健全です。
一言で言えば、バラバラに標準化しない場合、ドメイン全体 (集団) に関するステートメントを「結合」し、個人に関するステートメントを作成します。これはより弱くなり、以前に暗示されていたいくつかの事実を暗示しなくなります。それらは失われ、手続きは完了しません。
于 2015-03-13T00:31:45.097 に答える