一次ロジック解決統合

Question

節の形式で知識ベースの一部を示したと仮定します。

[1] p1(banana).

[2] not p1(X) or p2(Y).
[3] p1(X) or not p3(F).

...そしてその他のルール。

ほとんどの本は、次のようなことをします：

[1,2] {X=banana} p2(Y).

そしてより多くのステップ。

最初の質問：次のようなことをすることは等しく正しいですか：

[2,3] {X=X} p2(Y) or not p3(F).

そして、解決を続けます。

2番目の質問：各句で異なる変数が使用された場合、私は上記と同じことをすることができます。たとえば、：

[2] not p1(X1) or p2(Y1).
[3] p1(X2) or not p3(F2).

[2,3] {X1=X2} p2(Y) or not p3(F2).

前もって感謝します

Answer 1

ここで$ x $が原子命題ではなく変数であると仮定すると、最初に2と3の定量化を指定する必要があります。

$ forall x、y neg p1（x） vee p2（y）$、および同様に3についても、この場合、できることは$ x $と$ y $を利用可能な各原子提案に置き換えることです。命題の知識ベースを取得し、それに取り組むために。

2,3で提案することは、普遍的な定量化の下でのみ健全ですが、普遍的な定量化のみがある場合、それは確かに役立ちます。

2番目の質問については、変数の名前は何も意味しないため、あなたの代替もそこにも健全です。実際、クレーム$ forall y、p（y）$は、$ forall z、p（z）$に相当します。それがあなたを幸せにするなら、あなたは最初に名前を変更することができます:)

通常、解像度ガイド付きの証明では、定量化されたルールで具体的な表現を解決する方が有用であることに注意してください。たとえば、$ p（a）$を$ forall xp（x）からq（x）$で解決して、$ q（a）$を取得します。これは、（ヒューリスティックな）主張の証拠にあなたを導く可能性が高いです。