1

次回の試験について、次のレビュー用の質問があります。サポートが必要です。「メアリーは青リンゴだけを使ってパイを作る」という質問に、解像度を使って答える必要があります。私の現在の知識ベースと言語は次の文章です。

Mary only uses apples from John to make pies:
 ∀π,a(Apple(a) ∧ Pie(π) ∧ Make(M,π,a) => Grows(J,a))
(⌐Apple(a) V ⌐Pie(π) V ⌐Make(M, π, a) V Grows(J,a))    (in CNF)

最新の更新：

一般的にはもっと具体的にしようと思います。私が証明したいのは、「メアリーはパイを作るのに青リンゴだけを使う」ということです。このロジックを書くと、次のようになります。

メアリーは、青リンゴのみを使用してパイを作成します。π、aPie（π）A Make（M、π、a）=> Green（a）

そして、それをCNF形式（http://en.wikipedia.org/wiki/Conjunctive_normal_form）に変換する手順：

π,a ⌐(Pie(π) A Make(M, π, a)) V Green(a) 
π,a (⌐Pie(π) V ⌐Make(M, π, a)) V Green(a) 
(⌐Pie(π) V ⌐Make(M, π, a)) V Green(a) 
⌐Pie(π) V ⌐Make(M, π, a) V Green(a) (CNF form)

CNF形式でのこのステートメントの否定（証明の解決に使用します）：

Pie（π）A Make（M、π、a）A⌐Green（a）

一階述語論理に解決を使用する場合：（http://en.wikipedia.org/wiki/Resolution_(logic））

これは正しいですか！？それとも私はそれを間違えていますか？

4

2 に答える 2

1

問題に正しく取り組んでいるかどうかはわかりません。最初のステップは、3つのステートメント（「リンゴは緑または赤のいずれか」、「ジョンは緑のリンゴのみを栽培する」、「メアリーはジョンのリンゴのみを使用してパイを作る」）を、まだ行っていない節の形式にエンコードすることです。

2番目のステップは、証明しようとしているステートメントの否定（「メアリーはパイを作るために青リンゴのみを使用する」）も句の形式にエンコードすることです。私はあなたがそれをしたとは思わない、私はあなたが肯定的な声明をエンコードしたと思う。おそらく私は何かが欠けています。ただし、クエリステートメントの否定をエンコードすると、4つの短いステートメントがANDでつながれ、それぞれがナレッジベースのステートメントとして扱うことができます。

そこから、削減は機械的です。

更新： もう一度、証明しようとしているステートメントの否定を追加する必要があります。あなたはそれをしていません、あなたはステートメント自体とリンゴが緑色であるという別のステートメントを追加しています。そうしないでください。あなたはリンゴが緑色であるという声明を証明しようとしているのではなく、パイを作るために緑色のリンゴだけを使用しているメアリーについての声明を証明しようとしているのです。そのステートメントを否定し、他の3つのナレッジベースステートメントで解決し、矛盾を抽出します（つまり、一部のステートメントXについてXとnot-Xを一緒に解決します）。

それがアルゴリズムです。できます。そうしないと、「必要」かどうかに関係なく、解決アルゴリズム以外のことをしていることになります。宿題や試験を採点した場合、それは正しくないものとして採点されます。

アップデート2：近づいていますが、他のステートメントのいくつかがすでに持っているように、クエリステートメントにはApple（つまり、Apple（a））であることについての追加の句が必要です。ジョンのリンゴのみを使用しているメアリーに関するステートメントとほぼ同じように見えるはずです（クエリであるため否定されます）。その形式は正しく、小さな句がANDでつながれているため、1つが欠落しているだけです。

ただし、それができたら、これらの小さな句のそれぞれが（ANDと一緒につながれているため）ナレッジベースで独立したステートメントとして機能できることに注意してください。したがって、たとえば、今作成した方法で、3番目のステートメントの式を使用してPie（p）を解決できます。解決証明には多くのステップがありますが、クエリ否定を完全にエンコードすると、それらはすべてそのような小さなステップになります。

于 2012-06-10T17:16:43.230 に答える
1

一般的な情報として、CNFの知識ベースと、NEGATEDの目標（これもCNF）が必要です。次に、解決策を統合して適用することにより、解決策をゼロにするか、目標状態自体を設定する必要があります。他のオプションは、これらのいずれかを見つけて無限に解決することができないことです。

もしも

Make(p,π,a)

はナレッジベースにあり、解決策を最後の解決策と統合して適用します。

⌐Make(M,π,a)

あなたにゼロの解決策を与えます。この時点で、停止して結論を​​出すことができます。

于 2012-06-11T15:39:26.070 に答える