論理式を節形式に変換

このような問題を出題されたのですが
(1) ∀x∀y∀z[P(x,y)∧q(y,z)→r(x,z)]
(2)∀x[P(x)→(∃y∀z(q(y,z)→r(x,y)∨S(z)))]

(1)
=∀x∀y∀z～(P(x,y)∧q(y,z)∨r(y,z))
=∀x∀y∀z～P(x,y)∨～q(y,z)∨r(x,z)
=～P(x,y)∨～q(y,z)∨r(x,z)
(1)はこのように解いたのですがあっているでしょうか？
(2)の問題の解き方がよく分からずに困っています どなたか変換の過程を教えてください。
どうぞよろしくお願いします。

No.1 ベストアンサー 回答者： stomachman 回答日時： 2017/06/04 06:57

(2) ∀x[P(x)→(∃y∀z(q(y,z)→r(x,y)∨S(z)))]

限量子を外へ移動。
　　∀x∃y∀z[P(x)→((q(y,z)→r(x,y)∨S(z)))]
内側の→を展開
　　∀x∃y∀z[P(x)→((〜q(y,z)∨r(x,y)∨S(z)))]
外側の→を展開
　　∀x∃y∀z[〜P(x)∨((〜q(y,z)∨r(x,y)∨S(z)))]
よけいな括弧を削除
　　∀x∃y∀z[〜P(x)∨〜q(y,z)∨r(x,y)∨S(z)]
　(1)の最後で∀が全部除かれているところを見ると、自動導出の前処理の話だろう。ならば、yをスコーレム関数y(x)で置き換えれば終わり。

この回答へのお礼

お礼申し上げるのが遅くなり申し訳ございません　ありがとうございました。

お礼日時：2017/06/11 12:54