FC2ブログ
--.--
--
上記の広告は1ヶ月以上更新のないブログに表示されています。
新しい記事を書く事で広告が消せます。

01.15
Tue
導出反駁木を用いてある論理式が論理的帰結となっているかを知らべる方法をメモ

論理式
P⊃Q
Q⊃R

から
P⊃R

を導くのは妥当であるか

まず2つを節形式に直して P⊃R の否定の節から導出原理を用いて空節が導かれる事を確かめます

節はそれぞれ

¬P∨Q , ¬Q∨R , P , ¬Rとなります

resolution3.gif

もしくは

((P⊃Q)∧(Q⊃R))⊃(P⊃R)

が恒真式になることを確かめてもいいのかもしれません

これを命題論理の場合はこんな感じに命題変数を消してけばいいんですけど

述語論理になると、ユニフィケーション(変数に代入みたいの)をしなければいけません

さらに節が多くなってくるとどれを親節にするかですごく大変になったりするみたいです


簡単な例をやってみます

∀x(human(x)⊃mortal(x))
human(socrates)

から

∃x(mortal(x))

で、誰が死ぬのか調べます

∀x(human(x)⊃mortal(x))≡∀x(¬human(x)∨mortal(x))



∃x(mortal(x)) の否定は ∀x(¬mortal(x))

なので

これらの母式の節から導出反駁木をつくると

resolution4.gif

ということでsocratesが死ぬ存在であることがわかります
スポンサーサイト

comment 0 trackback 0
トラックバックURL
http://telracsmoratori.blog.fc2.com/tb.php/158-2d44c511
トラックバック
コメント
管理者にだけ表示を許可する
 
上記広告は1ヶ月以上更新のないブログに表示されています。新しい記事を書くことで広告を消せます。